Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ add_SNo (ordsucc x0) x2 = ordsucc (add_SNo x0 x2)) ⟶ SNo x0 ⟶ SNo x1 ⟶ ordinal (add_SNo x0 x1) ⟶ ordinal (ordsucc x0) ⟶ SNo (ordsucc x0) ⟶ ordinal (add_SNo (ordsucc x0) x1) ⟶ ordsucc (add_SNo x0 x1) ∈ add_SNo (ordsucc x0) x1 ⟶ not (ordinal (ordsucc (add_SNo x0 x1)))

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_SNo_ordinal_SL__11__9

proofgold address
TMdkj..^{Conj_add_SNo_ordinal_SL__11__9}

creator
35053 PrNpY../61091..

owner
35061 PrNpY../7991a..

term root
4e932..