Search for blocks/addresses/...

Proofgold Proof

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