Let x0 of type ι be given.

Assume H0: Subq x0 (Union 0).

Claim L1: x0 = 0

Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with x0.

Let x1 of type ι be given.

Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with x1, x0.

Assume H1: In x1 x0.

Claim L2: In x1 (Union 0)

Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x0, Union 0, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with 0, x1, False leaving 2 subgoals.

The subproof is completed by applying L2.

Let x2 of type ι be given.

Assume H3: In x1 x2.

Assume H4: In x2 0.

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x2.

The subproof is completed by applying H4.

Let x1 of type ι be given.

Apply L1 with λ x2 x3 . In x1 x3 ⟶ and (∀ x4 . not (exactly5 x3) ⟶ ∃ x5 . and (Subq x5 x3) (∀ x6 . In x6 0 ⟶ not (ordinal x4))) (∃ x4 . and (In x4 x1) (∃ x5 . not (TransSet x1))) ⟶ atleast4 x1.

Assume H2: In x1 0.

Apply FalseE with and (∀ x2 . not (exactly5 0) ⟶ ∃ x3 . and (Subq x3 0) (∀ x4 . In x4 0 ⟶ not (ordinal x2))) (∃ x2 . and (In x2 x1) (∃ x3 . not (TransSet x1))) ⟶ atleast4 x1.

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x1.

The subproof is completed by applying H2.

■

Proofgold Proof