Proofgold Proposition

∀ x0 . TransSet x0 ⟶ ZF_closed x0 ⟶ ∀ x1 . x1 ⊆ x0 ⟶ nIn x1 x0 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . bij (Sep x0 ordinal) x1 x3 ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
TarskiA_bij_ord

proof
PUdSr..

Megalodon
-

proofgold address
TMKg9..

creator
11630 PrGxv../2b48e..

owner
11630 PrGxv../2b48e..

term root
8aa76..