Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Assume H2: ∀ x2 . x2 ∈ x1 ⟶ add_SNo (ordsucc x0) x2 = ordsucc (add_SNo x0 x2).
Assume H3: SNo x0.
Assume H4: SNo x1.
Assume H5: ordinal (add_SNo x0 x1).
Assume H6: ordinal (ordsucc x0).
Assume H7: SNo (ordsucc x0).
Assume H8: ordinal (add_SNo (ordsucc x0) x1).
Assume H9: ordsucc (add_SNo x0 x1) ∈ add_SNo (ordsucc x0) x1.
Assume H10: ordinal (ordsucc (add_SNo x0 x1)).
Apply In_irref with ordsucc (add_SNo x0 x1).
Apply add_SNo_ordinal_SL with x0, x1, λ x2 x3 . ordsucc (add_SNo x0 x1) ∈ x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
■