Proofgold Proposition

∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 x4 : ι → ο . ordinal x2 ⟶ TransSet x2 ⟶ (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 : ι → ο . not (PNo_strict_imv x0 x1 x5 x6)) ⟶ PNo_strict_lowerbd x1 x2 x3 ⟶ PNo_strict_upperbd x0 x2 x4 ⟶ PNo_strict_lowerbd x1 x2 x4 ⟶ (∀ x5 . ordinal x5 ⟶ x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5)) ⟶ ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5)

type
prop

theory
HotG

name
-

proof
PURzn..

Megalodon
Conj_PNo_strict_imv_pred_eq__6__3

proofgold address
TMTmA..^{Conj_PNo_strict_imv_pred_eq__6__3}

creator
35045 PrNpY../a8271..

owner
35047 PrNpY../5bc17..

term root
74061..