Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Claim L1: ordinal (SNoLev x0)
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
Claim L2: ∀ x1 . x1 ∈ SNoL x0 ⟶ SNo x1
Let x1 of type ι be given.
Assume H2: x1 ∈ SNoL x0.
Claim L3: x1 ∈ SNoS_ (SNoLev x0)
Apply SepE1 with SNoS_ (SNoLev x0), λ x2 . SNoLt x2 x0, x1.
The subproof is completed by applying H2.
Apply SNoS_E with SNoLev x0, x1, ∃ x2 . and (ordinal x2) (SNo_ x2 x1) leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L3.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (x3 ∈ SNoLev x0) (SNo_ x3 x1)) x2.
Apply H4 with ∃ x3 . and (ordinal x3) (SNo_ x3 x1).
Assume H5: x2 ∈ SNoLev x0.
Assume H6: SNo_ x2 x1.
Let x3 of type ο be given.
Assume H7: ∀ x4 . and (ordinal x4) (SNo_ x4 x1) ⟶ x3.
Apply H7 with x2.
Apply andI with ordinal x2, SNo_ x2 x1 leaving 2 subgoals.
Apply ordinal_Hered with SNoLev x0, x2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Claim L3: ∀ x1 . x1 ∈ SNoR x0 ⟶ SNo x1
Let x1 of type ι be given.
Assume H3: x1 ∈ SNoR x0.
Claim L4: x1 ∈ SNoS_ (SNoLev x0)
Apply SepE1 with SNoS_ (SNoLev x0), λ x2 . SNoLt x0 x2, x1.
The subproof is completed by applying H3.
Apply SNoS_E with SNoLev x0, x1, ∃ x2 . and (ordinal x2) (SNo_ x2 x1) leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Assume H5: (λ x3 . and (x3 ∈ SNoLev x0) (SNo_ x3 x1)) x2.
Apply H5 with ∃ x3 . and (ordinal x3) (SNo_ x3 x1).
Assume H6: x2 ∈ SNoLev x0.
Assume H7: SNo_ x2 x1.
Let x3 of type ο be given.
Assume H8: ∀ x4 . and (ordinal x4) (SNo_ x4 x1) ⟶ x3.
Apply H8 with x2.
Apply andI with ordinal x2, SNo_ x2 x1 leaving 2 subgoals.
Apply ordinal_Hered with SNoLev x0, x2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Claim L4: ∀ x1 . x1 ∈ SNoL x0 ⟶ ∀ x2 . x2 ∈ SNoR x0 ⟶ SNoLt x1 x2
Let x1 of type ι be given.
Assume H4: x1 ∈ SNoL x0.
Let x2 of type ι be given.
Assume H5: x2 ∈ SNoR x0.
Apply SNoLt_tra with x1, x0, x2 leaving 5 subgoals.
Apply L2 with x1.
The subproof is completed by applying H4.
The subproof is completed by applying H0.
Apply L3 with x2.
The subproof is completed by applying H5.
Apply SepE2 with SNoS_ (SNoLev x0), λ x3 . SNoLt x3 x0, x1.
The subproof is completed by applying H4.
Apply SepE2 with SNoS_ (SNoLev x0), λ x3 . SNoLt x0 x3, x2.
The subproof is completed by applying H5.
Apply and3I with ∀ x1 . x1 ∈ SNoL x0 ⟶ SNo x1, ∀ x1 . x1 ∈ SNoR x0 ⟶ SNo x1, ∀ x1 . x1 ∈ SNoL x0 ⟶ ∀ x2 . x2 ∈ SNoR x0 ⟶ SNoLt x1 x2 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
■