Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ x0.
Let x1 of type ι be given.
Assume H2: x1 ⊆ SNoS_ x0.
Let x2 of type ι be given.
Assume H3: x2 ⊆ SNoS_ x0.
Assume H4: SNoCutP x1 x2.
Apply SNoCutP_SNoCut_impred with x1, x2, SNoLev (SNoCut x1 x2) ∈ ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H5: SNo (SNoCut x1 x2).
Assume H6: SNoLev (SNoCut x1 x2) ∈ ordsucc (binunion (famunion x1 (λ x3 . ordsucc (SNoLev x3))) (famunion x2 (λ x3 . ordsucc (SNoLev x3)))).
Assume H7: ∀ x3 . x3 ∈ x1 ⟶ SNoLt x3 (SNoCut x1 x2).
Assume H8: ∀ x3 . x3 ∈ x2 ⟶ SNoLt (SNoCut x1 x2) x3.
Assume H9: ∀ x3 . SNo x3 ⟶ (∀ x4 . x4 ∈ x1 ⟶ SNoLt x4 x3) ⟶ (∀ x4 . x4 ∈ x2 ⟶ SNoLt x3 x4) ⟶ and (SNoLev (SNoCut x1 x2) ⊆ SNoLev x3) (SNoEq_ (SNoLev (SNoCut x1 x2)) (SNoCut x1 x2) x3).
Apply ordinal_ordsucc_In_Subq with ordsucc x0, binunion (famunion x1 (λ x3 . ordsucc (SNoLev x3))) (famunion x2 (λ x3 . ordsucc (SNoLev x3))), SNoLev (SNoCut x1 x2) leaving 3 subgoals.
Apply ordinal_ordsucc with x0.
The subproof is completed by applying H0.
Apply ordinal_In_Or_Subq with binunion (famunion x1 (λ x3 . ordsucc (SNoLev x3))) (famunion x2 (λ x3 . ordsucc (SNoLev x3))), ordsucc x0, binunion (famunion x1 (λ x3 . ordsucc (SNoLev x3))) (famunion x2 (λ x3 . ordsucc (SNoLev x3))) ∈ ordsucc x0 leaving 4 subgoals.
Apply ordinal_binunion with famunion x1 (λ x3 . ordsucc (SNoLev x3)), famunion x2 (λ x3 . ordsucc (SNoLev x3)) leaving 2 subgoals.
Apply ordinal_famunion with x1, λ x3 . ordsucc (SNoLev x3).
Let x3 of type ι be given.
Assume H10: x3 ∈ x1.
Apply SNoS_E2 with x0, x3, ordinal ((λ x4 . ordsucc (SNoLev x4)) x3) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply H2 with x3.
The subproof is completed by applying H10.
Assume H11: SNoLev x3 ∈ x0.
Assume H12: ordinal (SNoLev x3).
Assume H13: SNo x3.
Assume H14: SNo_ (SNoLev x3) x3.
Apply ordinal_ordsucc with SNoLev x3.
The subproof is completed by applying H12.
Apply ordinal_famunion with x2, λ x3 . ordsucc (SNoLev x3).
Let x3 of type ι be given.
Assume H10: x3 ∈ x2.
Apply SNoS_E2 with x0, x3, ordinal ((λ x4 . ordsucc (SNoLev x4)) x3) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply H3 with x3.
The subproof is completed by applying H10.
Assume H11: SNoLev x3 ∈ x0.
Assume H12: ordinal (SNoLev x3).
Assume H13: SNo x3.
Assume H14: SNo_ (SNoLev x3) x3.
Apply ordinal_ordsucc with SNoLev x3.
The subproof is completed by applying H12.
Apply ordinal_ordsucc with x0.
The subproof is completed by applying H0.
Assume H10: binunion (famunion x1 (λ x3 . ordsucc (SNoLev x3))) (famunion ... ...) ∈ ....
...
...
...
■