Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
ordinal_trichotomy_or_impred

proof
PUcff..

Megalodon
ordinal_trichotomy_or_impred

proofgold address
TMX8g..^{ordinal_trichotomy_or_impred}

creator
4971 Pr6Pc../99acd..

owner
4971 Pr6Pc../99acd..

term root
7c0f0..