Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ∀ x1 . In x1 x0 ⟶ ordinal x1.
Apply unknownprop_5273a64cd2d40c560fbf5871c7601206337acc93fe8f7292cc8c65a171682421 with λ x1 x2 : ι → ο . x2 (Union x0).
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with TransSet (Union x0), ∀ x1 . In x1 (Union x0) ⟶ TransSet x1 leaving 2 subgoals.
Apply unknownprop_867ee8b2da9f256b3418dab3ba4978d6cabdc87fec1095d8f8aa46324a9136f8 with Union x0.
Let x1 of type ι be given.
Assume H1: In x1 (Union x0).
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with x0, x1, Subq x1 (Union x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: In x1 x2.
Assume H3: In x2 x0.
Claim L4: ordinal x2
Apply H0 with x2.
The subproof is completed by applying H3.
Claim L5: TransSet x2
Apply unknownprop_e682831a7124f89af4a1b1d248afbcd452dfbbb9d90b9a88db6885fe36808b65 with x2.
The subproof is completed by applying L4.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with x1, Union x0.
Let x3 of type ι be given.
Assume H6: In x3 x1.
Claim L7: In x3 x2
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x1, x2, x3 leaving 2 subgoals.
Apply unknownprop_5af24edc592c6d7fa3cf53e40211635bbed8f39380469ac8aef3490ee700739c with x2, x1 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with x0, x3, x2 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H1: In x1 (Union x0).
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with x0, x1, TransSet x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: In x1 x2.
Assume H3: In x2 x0.
Claim L4: ordinal x2
Apply H0 with x2.
The subproof is completed by applying H3.
Claim L5: ordinal x1
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with x2, x1 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
Apply unknownprop_e682831a7124f89af4a1b1d248afbcd452dfbbb9d90b9a88db6885fe36808b65 with x1.
The subproof is completed by applying L5.
■