Search for blocks/addresses/...

Proofgold Proof

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