Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 . ordinal x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 . x3 ∈ SNoS_ x1 ⟶ ∀ x4 . x4 ∈ SNoS_ x2 ⟶ x0 x3 x4.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1: SNo x1.
Assume H2: SNo x2.
Claim L3: ordinal (SNoLev x1)
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H1.
Claim L4: ordinal (ordsucc (SNoLev x1))
Apply ordinal_ordsucc with SNoLev x1.
The subproof is completed by applying L3.
Claim L5: x1 ∈ SNoS_ (ordsucc (SNoLev x1))
Apply SNoS_SNoLev with x1.
The subproof is completed by applying H1.
Claim L6: ordinal (SNoLev x2)
Apply SNoLev_ordinal with x2.
The subproof is completed by applying H2.
Claim L7: ordinal (ordsucc (SNoLev x2))
Apply ordinal_ordsucc with SNoLev x2.
The subproof is completed by applying L6.
Claim L8: x2 ∈ SNoS_ (ordsucc (SNoLev x2))
Apply SNoS_SNoLev with x2.
The subproof is completed by applying H2.
Apply H0 with ordsucc (SNoLev x1), ordsucc (SNoLev x2), x1, x2 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L7.
The subproof is completed by applying L5.
The subproof is completed by applying L8.
■