Metamath Proof Explorer

Theorem ordtype2

Description: For any set-like well-ordered class, if the order isomorphism exists (is a set), then it maps some ordinal onto A isomorphically. Otherwise, F is a proper class, which implies that either ran F C_ A is a proper class or dom F = On . This weak version of ordtype does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 ⊢F=OrdIsoRA
Assertion ordtype2 ⊢RWeA∧RSeA∧F∈V→FIsomE,Rdom⁡FA

Proof

Step Hyp Ref Expression
1 oicl.1 ⊢F=OrdIsoRA
2 eqid ⊢recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
3 eqid ⊢w∈A|∀j∈ran⁡hjRw=w∈A|∀j∈ran⁡hjRw
4 eqid ⊢h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv=h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
5 2 3 4 ordtypecbv ⊢recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRs=recs⁡h∈V⟼ιv∈w∈A|∀j∈ran⁡hjRw|∀u∈w∈A|∀j∈ran⁡hjRw¬uRv
6 eqid ⊢x∈On|∃t∈A∀z∈recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRsxzRt=x∈On|∃t∈A∀z∈recs⁡f∈V⟼ιs∈y∈A|∀i∈ran⁡fiRy|∀r∈y∈A|∀i∈ran⁡fiRy¬rRsxzRt
7 simp1 ⊢RWeA∧RSeA∧F∈V→RWeA
8 simp2 ⊢RWeA∧RSeA∧F∈V→RSeA
9 simp3 ⊢RWeA∧RSeA∧F∈V→F∈V
10 5 3 4 6 1 7 8 9 ordtypelem9 ⊢RWeA∧RSeA∧F∈V→FIsomE,Rdom⁡FA