Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ real.
Let x1 of type ι be given.
Assume H1: x1 ⊆ real.
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).
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Apply SNoCutP_SNoCut_impred with famunion omega (λ x2 . (λ x3 . {x4 ∈ SNoS_ x3|∃ x5 . and (x5 ∈ x0) ...}) ...), ..., ... leaving 2 subgoals.
...
...
■