Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: Field x0.

Let x1 of type ι be given.

Claim L1: not (and (x1 ∈ field0 x0) (field3 x0 ∈ setminus (field0 x0) (Sing (field3 x0))))

Assume H1: and (x1 ∈ field0 x0) (field3 x0 ∈ setminus (field0 x0) (Sing (field3 x0))).

Apply H1 with False.

Assume H2: x1 ∈ field0 x0.

Assume H3: field3 x0 ∈ setminus (field0 x0) (Sing (field3 x0)).

Apply setminusE with field0 x0, Sing (field3 x0), field3 x0, False leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: field3 x0 ∈ field0 x0.

Assume H5: nIn (field3 x0) (Sing (field3 x0)).

Apply H5.

The subproof is completed by applying SingI with field3 x0.

Apply If_i_0 with and (x1 ∈ field0 x0) (field3 x0 ∈ setminus (field0 x0) (Sing (field3 x0))), prim0 (λ x2 . and (x2 ∈ field0 x0) (x1 = field2b x0 (field3 x0) x2)), 0.

The subproof is completed by applying L1.

■