Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: 1 ∈ x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H2: 68498.. x0 x1.
Assume H3: binunion x1 {(λ x6 . SetAdjoin x6 (Sing x0)) x5|x5 ∈ x3} = binunion x2 {(λ x6 . SetAdjoin x6 (Sing x0)) x5|x5 ∈ x4}.
Let x5 of type ι be given.
Assume H4: x5 ∈ x1.
Claim L5: ...
...
Apply binunionE with x2, {(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x4}, x5, x5 ∈ x2 leaving 3 subgoals.
The subproof is completed by applying L5.
Assume H6: x5 ∈ x2.
The subproof is completed by applying H6.
Assume H6: x5 ∈ {(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x4}.
Apply FalseE with x5 ∈ x2.
Apply ReplE_impred with x4, λ x6 . SetAdjoin x6 (Sing x0), x5, False leaving 2 subgoals.
The subproof is completed by applying H6.
Let x6 of type ι be given.
Assume H7: x6 ∈ x4.
Assume H8: x5 = (λ x7 . SetAdjoin x7 (Sing x0)) x6.
Apply H2 with x5, False leaving 2 subgoals.
The subproof is completed by applying H4.
Let x7 of type ι be given.
Assume H9: (λ x8 . and (SNo x8) (or (x5 ∈ x8) (∃ x9 . and (x9 ∈ x8) (∃ x10 . and (x10 ∈ x0) (and (1 ∈ x10) (x5 = SetAdjoin x9 (Sing x10))))))) x7.
Apply H9 with False.
Assume H10: SNo x7.
Assume H11: or (x5 ∈ x7) (∃ x8 . and (x8 ∈ x7) (∃ x9 . and (x9 ∈ x0) (and (1 ∈ x9) (x5 = SetAdjoin x8 (Sing x9))))).
Apply H11 with False leaving 2 subgoals.
Assume H12: x5 ∈ x7.
Apply unknownprop_b77e4d13156bc801da7c50d615690a07853273eb1e278cd0903fec4370f9e4e2 with x0, x7, x6 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
Apply H8 with λ x8 x9 . x8 ∈ x7.
The subproof is completed by applying H12.
Assume H12: ∃ x8 . and (x8 ∈ x7) (∃ x9 . and (x9 ∈ x0) (and (1 ∈ x9) (x5 = SetAdjoin x8 (Sing x9)))).
Apply H12 with False.
Let x8 of type ι be given.
Assume H13: (λ x9 . and (x9 ∈ x7) (∃ x10 . and (x10 ∈ x0) (and (1 ∈ x10) (x5 = SetAdjoin x9 (Sing x10))))) x8.
Apply H13 with False.
Assume H14: x8 ∈ x7.
Assume H15: ∃ x9 . and (x9 ∈ x0) (and (1 ∈ x9) (x5 = SetAdjoin x8 (Sing x9))).
Apply H15 with False.
Let x9 of type ι be given.
Assume H16: (λ x10 . and (x10 ∈ x0) (and (1 ∈ x10) (x5 = SetAdjoin x8 (Sing x10)))) x9.
Apply H16 with False.
Assume H17: x9 ∈ x0.
Assume H18: and (1 ∈ x9) (x5 = SetAdjoin x8 (Sing x9)).
Apply H18 with False.
Assume H19: 1 ∈ x9.
Assume H20: x5 = SetAdjoin x8 (Sing x9).
Claim L21: ...
...
Apply unknownprop_6287073a7195e79c52abdc1556efdae70a83304a479aee56c6dfadb3bbee4870 with x0, x9, x6, x7, x8 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L21.
The subproof is completed by applying H10.
...
...
■