Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ SNoS_ omega.
Let x1 of type ι be given.
Assume H1: x1 ⊆ SNoS_ omega.
Assume H2: SNoCutP x0 x1.
Apply H2 with (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (x1 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∃ x3 . and (x3 ∈ x0) (SNoLt x2 x3)) ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∃ x3 . and (x3 ∈ x1) (SNoLt x3 x2)) ⟶ SNoCut x0 x1 ∈ real.
Assume H3: and (∀ x2 . x2 ∈ x0 ⟶ SNo x2) (∀ x2 . x2 ∈ x1 ⟶ SNo x2).
Apply H3 with (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (x1 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∃ x3 . and (x3 ∈ x0) (SNoLt x2 x3)) ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∃ x3 . and (x3 ∈ x1) (SNoLt x3 x2)) ⟶ SNoCut x0 x1 ∈ real.
Assume H4: ∀ x2 . x2 ∈ x0 ⟶ SNo x2.
Assume H5: ∀ x2 . x2 ∈ x1 ⟶ SNo x2.
Assume H6: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3.
Assume H7: x0 = 0 ⟶ ∀ x2 : ο . x2.
Assume H8: x1 = 0 ⟶ ∀ x2 : ο . x2.
Assume H9: ∀ x2 . x2 ∈ x0 ⟶ ∃ x3 . and (x3 ∈ x0) (SNoLt x2 x3).
Assume H10: ∀ x2 . x2 ∈ x1 ⟶ ∃ x3 . and (x3 ∈ x1) (SNoLt x3 x2).
Apply SNoCutP_SNoCut_impred with x0, x1, SNoCut x0 x1 ∈ real leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H11: SNo (SNoCut x0 x1).
Assume H12: SNoLev (SNoCut x0 x1) ∈ ordsucc (binunion (famunion x0 (λ x2 . ordsucc (SNoLev x2))) (famunion x1 (λ x2 . ordsucc (SNoLev x2)))).
Assume H13: ∀ x2 . x2 ∈ x0 ⟶ SNoLt x2 (SNoCut x0 x1).
Assume H14: ∀ x2 . x2 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x2.
Assume H15: ∀ x2 . SNo x2 ⟶ (∀ x3 . x3 ∈ x0 ⟶ SNoLt x3 x2) ⟶ (∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x2) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x2).
Apply ordsuccE with omega, SNoLev (SNoCut x0 x1), SNoCut x0 x1 ∈ ... leaving 3 subgoals.
...
...
...
■