Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ nIn x0 {SetAdjoin x2 (Sing 1)|x2 ∈ x1}

type
prop

theory
HotG

name
ordinal_notin_tagged_Repl

proof
PUUwp..

Megalodon
ordinal_notin_tagged_Repl

proofgold address
TMUFg..^{ordinal_notin_tagged_Repl}

creator
4910 Pr6Pc../e9320..

owner
4910 Pr6Pc../e9320..

term root
7f35b..