Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_e218ed8cf74f73d11b13279ecb43db2e902573ebd411cc1f7c1f71620f4a5da3 with real, prim4 omega leaving 2 subgoals.
Apply atleastp_tra with real, SNoS_ (ordsucc omega), prim4 omega leaving 2 subgoals.
Apply Subq_atleastp with real, SNoS_ (ordsucc omega).
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Apply real_E with x0, x0 ∈ SNoS_ (ordsucc omega) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: SNo x0.
Assume H2: SNoLev x0 ∈ ordsucc omega.
Assume H3: x0 ∈ SNoS_ (ordsucc omega).
Assume H4: SNoLt (minus_SNo omega) x0.
Assume H5: SNoLt x0 omega.
Assume H6: ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0.
Assume H7: ∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))).
Apply SNoS_I with ordsucc omega, x0, SNoLev x0 leaving 3 subgoals.
The subproof is completed by applying ordsucc_omega_ordinal.
The subproof is completed by applying H2.
Apply SNoLev_ with x0.
The subproof is completed by applying H1.
The subproof is completed by applying atleastp_SNoS_ordsucc_omega_Power_omega.
set y0 to be ...
set y1 to be ...
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Let x2 of type ο be given.
Assume H35: ∀ x3 : ι → ι . inj (prim4 omega) real x3 ⟶ x2.
Apply H35 with λ x3 . If_i (finite x3) (add_SNo ((λ x4 . binunion x4 (famunion x4 (λ x5 . {(λ x7 . SetAdjoin x7 (Sing 1)) x6|x6 ∈ x5,nIn x6 x4}))) ((λ x4 . binunion (Sing 0) {ordsucc x5|x5 ∈ x4}) x3)) 1) (If_i (finite (setminus omega x3)) (minus_SNo ((λ x4 . binunion x4 (famunion x4 (λ x5 . {(λ x7 . SetAdjoin x7 (Sing 1)) x6|x6 ∈ x5,nIn x6 x4}))) ((λ x4 . binunion (Sing 0) {ordsucc x5|x5 ∈ x4}) (setminus omega x3)))) (SNoCut ((λ x4 . famunion omega (λ x5 . y0 x4 x5)) x3) ((λ x4 . famunion omega (λ x5 . y1 x4 x5)) x3))).
Apply andI with ∀ x3 . ... ⟶ (λ x4 . If_i (finite x4) (add_SNo ((λ x5 . binunion x5 (famunion x5 (λ x6 . {(λ x8 . SetAdjoin x8 (Sing 1)) x7|x7 ∈ x6,nIn x7 x5}))) ((λ x5 . binunion (Sing 0) {ordsucc x6|x6 ∈ x5}) x4)) 1) (If_i (finite (setminus omega x4)) (minus_SNo ((λ x5 . binunion x5 (famunion x5 (λ x6 . {(λ x8 . SetAdjoin x8 (Sing 1)) x7|x7 ∈ x6,nIn x7 x5}))) ((λ x5 . binunion (Sing 0) {ordsucc x6|x6 ∈ x5}) (setminus omega x4)))) (SNoCut ((λ x5 . famunion omega (λ x6 . y0 x5 ...)) ...) ...))) ... ∈ ..., ... leaving 2 subgoals.
...
...
■