Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x1 ∈ ordsucc (SNoLev x2) ⟶ x2 = minus_SNo x3 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0.
Claim L1: ordinal (SNoLev 0)
Apply SNoLev_0 with λ x0 x1 . ordinal x1.
The subproof is completed by applying ordinal_Empty.
Claim L2: 0 ∈ ordsucc (SNoLev 0)
Apply SNoLev_0 with λ x0 x1 . 0 ∈ ordsucc x1.
The subproof is completed by applying In_0_1.
Claim L3: 0 = minus_SNo 0
Let x0 of type ι → ι → ο be given.
The subproof is completed by applying minus_SNo_0 with λ x1 x2 . x0 x2 x1.
Claim L4: SNoLev (minus_SNo 0) ⊆ SNoLev 0
Apply minus_SNo_Lev with 0, λ x0 x1 . x1 ⊆ SNoLev 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with λ x0 x1 . x1 ⊆ x1.
The subproof is completed by applying Subq_ref with 0.
Claim L5: ordinal (SNoLev (minus_SNo 0))
Apply minus_SNo_Lev with 0, λ x0 x1 . ordinal x1 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with λ x0 x1 . ordinal x1.
The subproof is completed by applying ordinal_Empty.
Claim L6: not (ordinal (ordsucc (SNoLev 0)) ⟶ 0 ∈ SNoLev 0)
Apply SNoLev_0 with λ x0 x1 . not (ordinal (ordsucc x1) ⟶ 0 ∈ x1).
Assume H6: ordinal 1 ⟶ 0 ∈ 0.
Apply In_irref with 0.
Apply H6.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
Apply L6.
Apply H0 with 0, 0, 0, 0 leaving 5 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
■