Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: ordinal x1.
Assume H1: ordinal x2.
Apply unknownprop_e5ee05cdff8551ce0d9dc58ec4d6754afa2e75276323e770f74710c8b0d2eef5 with x1, x0, SNo_ x2 x0 ⟶ Subq x1 x2.
Assume H2: Subq x0 (SNoElts_ x1).
Assume H3: ∀ x3 . In x3 x1 ⟶ exactly1of2 (In (SetAdjoin x3 (Sing 1)) x0) (In x3 x0).
Apply unknownprop_e5ee05cdff8551ce0d9dc58ec4d6754afa2e75276323e770f74710c8b0d2eef5 with x2, x0, Subq x1 x2.
Assume H4: Subq x0 (SNoElts_ x2).
Assume H5: ∀ x3 . In x3 x2 ⟶ exactly1of2 (In (SetAdjoin x3 (Sing 1)) x0) (In x3 x0).
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with x1, x2.
Let x3 of type ι be given.
Assume H6: In x3 x1.
Claim L7: ...
...
Apply unknownprop_22b63889168c3c27321f1d9d99a6c13d916b48d833ad1ef7079baee20e0a05c6 with In ((λ x4 . SetAdjoin x4 (Sing 1)) x3) x0, In x3 x0, In x3 x2 leaving 3 subgoals.
Apply H3 with x3.
The subproof is completed by applying H6.
Assume H8: In ((λ x4 . SetAdjoin x4 (Sing 1)) x3) x0.
Assume H9: not (In x3 x0).
Claim L10: ∀ x4 . In x4 (SNoElts_ x2) ⟶ x4 = (λ x5 . SetAdjoin x5 (Sing 1)) x3 ⟶ In x3 x2
Apply unknownprop_023b2e512ed9c52f995f2d07c1a06cfb4ae27f29745759c860f7e880eac7d40f with x2, λ x4 . x4 = (λ x5 . SetAdjoin x5 (Sing 1)) x3 ⟶ In x3 x2 leaving 2 subgoals.
Let x4 of type ι be given.
Assume H10: In x4 x2.
Assume H11: x4 = (λ x5 . SetAdjoin x5 (Sing 1)) x3.
Apply FalseE with In x3 x2.
Apply unknownprop_0016de04f44a712243c9eeee572a992709374894dd4f8741b2a55208a71b7c48 with x3.
Apply H11 with λ x5 x6 . ordinal x5.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
Let x4 of type ι be given.
Assume H10: In x4 x2.
Assume H11: (λ x5 . SetAdjoin x5 (Sing 1)) x4 = (λ x5 . SetAdjoin x5 (Sing 1)) x3.
Apply unknownprop_b1443874f1d94e8ae4702eeac0a8d34b82a3a5fa428acb67206d58ef176d9733 with x4, x3, λ x5 x6 . In x5 x2 leaving 4 subgoals.
Apply unknownprop_df95567eaac7dcf742571a06351d685ef037c3575a0b273f643efe646824ac1a with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
The subproof is completed by applying L7.
The subproof is completed by applying H11.
The subproof is completed by applying H10.
Apply L10 with (λ x4 . SetAdjoin x4 (Sing 1)) x3 leaving 2 subgoals.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x0, SNoElts_ x2, (λ x4 . SetAdjoin x4 (Sing 1)) x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Let x4 of type ι → ι → ο be given.
Assume H11: x4 (SetAdjoin x3 (Sing 1)) (SetAdjoin x3 (Sing 1)).
The subproof is completed by applying H11.
Assume H8: not (In (SetAdjoin x3 (Sing 1)) x0).
Assume H9: In x3 x0.
Claim L10: ∀ x4 . In x4 (SNoElts_ x2) ⟶ x4 = x3 ⟶ In x3 x2
Apply unknownprop_023b2e512ed9c52f995f2d07c1a06cfb4ae27f29745759c860f7e880eac7d40f with x2, λ x4 . x4 = x3 ⟶ In x3 x2 leaving 2 subgoals.
Let x4 of type ι be given.
Assume H10: In x4 x2.
Assume H11: x4 = x3.
Apply H11 with λ x5 x6 . In x5 x2.
The subproof is completed by applying H10.
Let x4 of type ι be given.
Assume H10: In x4 ....
...
Apply L10 with x3 leaving 2 subgoals.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x0, SNoElts_ x2, x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
Let x4 of type ι → ι → ο be given.
Assume H11: x4 x3 x3.
The subproof is completed by applying H11.
■