Let x0 of type ι be given.

Assume H0: Field x0.

Let x1 of type ι be given.

Assume H1: x1 ∈ K_field_0 x0 x0.

Let x2 of type ι be given.

Assume H2: x2 ∈ setminus (K_field_0 x0 x0) (Sing (K_field_3 x0 x0)).

Apply setminusE with K_field_0 x0 x0, Sing (K_field_3 x0 x0), x2, and (a4228.. x0 x1 x2 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 (a4228.. x0 x1 x2)) leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: x2 ∈ K_field_0 x0 x0.

Assume H4: nIn x2 (Sing (K_field_3 x0 x0)).

Claim L5: ...

...

Claim L6: ...

...

Claim L7: ∃ x3 . and (x3 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x3)

Apply unknownprop_42c10093362e32c14fc1fb0fe4cdcdf964fd23a080978018c8059be9c77cc7f2 with x0, x2, ∃ x3 . and (x3 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x3) leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

The subproof is completed by applying L5.

Let x3 of type ι be given.

Assume H7: (λ x4 . and (x4 ∈ K_field_0 x0 x0) (K_field_2_b x0 x0 x2 x4 = K_field_4 x0 x0)) x3.

Apply H7 with ∃ x4 . and (x4 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x4).

Assume H8: x3 ∈ K_field_0 x0 x0.

Assume H9: K_field_2_b x0 x0 x2 x3 = K_field_4 x0 x0.

Let x4 of type ο be given.

Assume H10: ∀ x5 . and (x5 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x5) ⟶ x4.

Apply H10 with K_field_2_b x0 x0 x3 x1.

Apply andI with K_field_2_b x0 x0 x3 x1 ∈ K_field_0 x0 x0, x1 = K_field_2_b x0 x0 x2 (K_field_2_b x0 x0 x3 x1) leaving 2 subgoals.

Apply unknownprop_6c6c06a9cf1d6d0ab75358a5bf72715769aad5016bd6e0ae821fb9de263b486a with x0, x3, x1 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H8.

The subproof is completed by applying H1.

Let x5 of type ι → ι → ο be given.

set y6 to be ...

set y7 to be ...

Claim L11: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6

Let x8 of type ι → ο be given.

Assume H11: x8 ....

...

set y8 to be λ x8 x9 . y7 x9 x8

Apply L11 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9.

Assume H12: y8 y7 y7.

The subproof is completed by applying H12.

Apply If_i_1 with and (x1 ∈ K_field_0 x0 x0) (x2 ∈ setminus (K_field_0 x0 x0) (Sing (K_field_3 x0 x0))), prim0 (λ x3 . and (x3 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x3)), 0, λ x3 x4 . and (x4 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x4) leaving 2 subgoals.

The subproof is completed by applying L6.

Apply Eps_i_ex with λ x3 . and (x3 ∈ K_field_0 x0 x0) (x1 = K_field_2_b x0 x0 x2 x3).

The subproof is completed by applying L7.

■

Proofgold Proof