Metamath Proof Explorer

Theorem oicl

Description: The order type of the well-order R on A is an ordinal. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 ⊢F=OrdIsoRA
Assertion oicl ⊢Ord⁡dom⁡F

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 ordtypelem5 ⊢RWeA∧RSeA→Ord⁡dom⁡F∧F:dom⁡F⟶A
10 9 simpld ⊢RWeA∧RSeA→Ord⁡dom⁡F
11 ord0 ⊢Ord⁡∅
12 1 oi0 ⊢¬RWeA∧RSeA→F=∅
13 12 dmeqd ⊢¬RWeA∧RSeA→dom⁡F=dom⁡∅
14 dm0 ⊢dom⁡∅=∅
15 13 14 eqtrdi ⊢¬RWeA∧RSeA→dom⁡F=∅
16 ordeq ⊢dom⁡F=∅→Ord⁡dom⁡F↔Ord⁡∅
17 15 16 syl ⊢¬RWeA∧RSeA→Ord⁡dom⁡F↔Ord⁡∅
18 11 17 mpbiri ⊢¬RWeA∧RSeA→Ord⁡dom⁡F
19 10 18 pm2.61i ⊢Ord⁡dom⁡F