Metamath Proof Explorer

Theorem ordtype

Description: For any set-like well-ordered class, there is an isomorphic ordinal number called its order type. (Contributed by Jeff Hankins, 17-Oct-2009) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 ⊢F=OrdIsoRA
Assertion ordtype ⊢RWeA∧RSeA→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 simpl ⊢RWeA∧RSeA→RWeA
8 simpr ⊢RWeA∧RSeA→RSeA
9 5 3 4 6 1 7 8 ordtypelem10 ⊢RWeA∧RSeA→FIsomE,Rdom⁡FA