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.
Assume H2: SNo_ x1 x0.
Assume H3: SNo_ x2 x0.
Let x3 of type ι be given.
Assume H4: x3 ∈ x1.
Apply H2 with x3 ∈ x2.
Assume H5: x0 ⊆ SNoElts_ x1.
Assume H6: ∀ x4 . x4 ∈ x1 ⟶ exactly1of2 (SetAdjoin x4 (Sing 1) ∈ x0) (x4 ∈ x0).
Apply H3 with x3 ∈ x2.
Assume H7: x0 ⊆ SNoElts_ x2.
Assume H8: ∀ x4 . x4 ∈ x2 ⟶ exactly1of2 (SetAdjoin x4 (Sing 1) ∈ x0) (x4 ∈ x0).
Claim L9: ordinal x3
Apply ordinal_Hered with x1, x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply exactly1of2_or with (λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ x0, x3 ∈ x0, x3 ∈ x2 leaving 3 subgoals.
Apply H6 with x3.
The subproof is completed by applying H4.
Assume H10: (λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ x0.
Claim L11: (λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ binunion x2 {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2}
Apply H7 with (λ x4 . SetAdjoin x4 (Sing 1)) x3.
The subproof is completed by applying H10.
Claim L12: or ((λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ x2) ((λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2})
Apply binunionE with x2, {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2}, (λ x4 . SetAdjoin x4 (Sing 1)) x3.
The subproof is completed by applying L11.
Apply L12 with x3 ∈ x2 leaving 2 subgoals.
Assume H13: (λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ x2.
Apply FalseE with x3 ∈ x2.
Apply tagged_notin_ordinal with x2, x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H13.
Assume H13: (λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2}.
Apply tagged_ReplE with x2, x3 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L9.
The subproof is completed by applying H13.
Assume H10: x3 ∈ x0.
Claim L11: x3 ∈ binunion x2 {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2}
Apply H7 with x3.
The subproof is completed by applying H10.
Claim L12: or (x3 ∈ x2) (x3 ∈ {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2})
Apply binunionE with x2, {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2}, x3.
The subproof is completed by applying L11.
Apply L12 with x3 ∈ x2 leaving 2 subgoals.
Assume H13: x3 ∈ x2.
The subproof is completed by applying H13.
Assume H13: x3 ∈ {(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x2}.
Apply FalseE with x3 ∈ x2.
Apply ordinal_notin_tagged_Repl with x3, x2 leaving 2 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying H13.
■