Metamath Proof Explorer

Theorem ordtypelem9

Description: Lemma for ordtype . Either the function OrdIso is an isomorphism onto all of A , or OrdIso is not a set, which by oif implies that either ran O C_ A is a proper class or dom O = On . (Contributed by Mario Carneiro, 25-Jun-2015) (Revised by AV, 28-Jul-2024)

Ref Expression
Hypotheses ordtypelem.1 ⊢F=recs⁡G
ordtypelem.2 ⊢C=w∈A|∀j∈ran⁡hjRw
ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
ordtypelem.5 ⊢T=x∈On|∃t∈A∀z∈FxzRt
ordtypelem.6 ⊢O=OrdIsoRA
ordtypelem.7 ⊢φ→RWeA
ordtypelem.8 ⊢φ→RSeA
ordtypelem9.1 ⊢φ→O∈V
Assertion ordtypelem9 ⊢φ→OIsomE,Rdom⁡OA

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢F=recs⁡G
2 ordtypelem.2 ⊢C=w∈A|∀j∈ran⁡hjRw
3 ordtypelem.3 ⊢G=h∈V⟼ιv∈C|∀u∈C¬uRv
4 ordtypelem.5 ⊢T=x∈On|∃t∈A∀z∈FxzRt
5 ordtypelem.6 ⊢O=OrdIsoRA
6 ordtypelem.7 ⊢φ→RWeA
7 ordtypelem.8 ⊢φ→RSeA
8 ordtypelem9.1 ⊢φ→O∈V
9 1 2 3 4 5 6 7 ordtypelem8 ⊢φ→OIsomE,Rdom⁡Oran⁡O
10 1 2 3 4 5 6 7 ordtypelem4 ⊢φ→O:T∩dom⁡F⟶A
11 10 frnd ⊢φ→ran⁡O⊆A
12 1 2 3 4 5 6 7 ordtypelem2 ⊢φ→Ord⁡T
13 ordirr ⊢Ord⁡T→¬T∈T
14 12 13 syl ⊢φ→¬T∈T
15 1 tfr1a ⊢Fun⁡F∧Lim⁡dom⁡F
16 15 simpri ⊢Lim⁡dom⁡F
17 limord ⊢Lim⁡dom⁡F→Ord⁡dom⁡F
18 16 17 ax-mp ⊢Ord⁡dom⁡F
19 1 2 3 4 5 6 7 ordtypelem1 ⊢φ→O=F↾T
20 8 elexd ⊢φ→O∈V
21 19 20 eqeltrrd ⊢φ→F↾T∈V
22 1 tfr2b ⊢Ord⁡T→T∈dom⁡F↔F↾T∈V
23 12 22 syl ⊢φ→T∈dom⁡F↔F↾T∈V
24 21 23 mpbird ⊢φ→T∈dom⁡F
25 ordelon ⊢Ord⁡dom⁡F∧T∈dom⁡F→T∈On
26 18 24 25 sylancr ⊢φ→T∈On
27 imaeq2 ⊢a=T→Fa=FT
28 27 raleqdv ⊢a=T→∀c∈FacRb↔∀c∈FTcRb
29 28 rexbidv ⊢a=T→∃b∈A∀c∈FacRb↔∃b∈A∀c∈FTcRb
30 breq1 ⊢z=c→zRt↔cRt
31 30 cbvralvw ⊢∀z∈FxzRt↔∀c∈FxcRt
32 breq2 ⊢t=b→cRt↔cRb
33 32 ralbidv ⊢t=b→∀c∈FxcRt↔∀c∈FxcRb
34 31 33 bitrid ⊢t=b→∀z∈FxzRt↔∀c∈FxcRb
35 34 cbvrexvw ⊢∃t∈A∀z∈FxzRt↔∃b∈A∀c∈FxcRb
36 imaeq2 ⊢x=a→Fx=Fa
37 36 raleqdv ⊢x=a→∀c∈FxcRb↔∀c∈FacRb
38 37 rexbidv ⊢x=a→∃b∈A∀c∈FxcRb↔∃b∈A∀c∈FacRb
39 35 38 bitrid ⊢x=a→∃t∈A∀z∈FxzRt↔∃b∈A∀c∈FacRb
40 39 cbvrabv ⊢x∈On|∃t∈A∀z∈FxzRt=a∈On|∃b∈A∀c∈FacRb
41 4 40 eqtri ⊢T=a∈On|∃b∈A∀c∈FacRb
42 29 41 elrab2 ⊢T∈T↔T∈On∧∃b∈A∀c∈FTcRb
43 42 baib ⊢T∈On→T∈T↔∃b∈A∀c∈FTcRb
44 26 43 syl ⊢φ→T∈T↔∃b∈A∀c∈FTcRb
45 14 44 mtbid ⊢φ→¬∃b∈A∀c∈FTcRb
46 ralnex ⊢∀b∈A¬∀c∈FTcRb↔¬∃b∈A∀c∈FTcRb
47 45 46 sylibr ⊢φ→∀b∈A¬∀c∈FTcRb
48 47 r19.21bi ⊢φ∧b∈A→¬∀c∈FTcRb
49 19 rneqd ⊢φ→ran⁡O=ran⁡F↾T
50 df-ima ⊢FT=ran⁡F↾T
51 49 50 eqtr4di ⊢φ→ran⁡O=FT
52 51 adantr ⊢φ∧b∈A→ran⁡O=FT
53 52 raleqdv ⊢φ∧b∈A→∀c∈ran⁡OcRb↔∀c∈FTcRb
54 10 ffund ⊢φ→Fun⁡O
55 54 funfnd ⊢φ→OFndom⁡O
56 55 adantr ⊢φ∧b∈A→OFndom⁡O
57 breq1 ⊢c=O⁡m→cRb↔O⁡mRb
58 57 ralrn ⊢OFndom⁡O→∀c∈ran⁡OcRb↔∀m∈dom⁡OO⁡mRb
59 56 58 syl ⊢φ∧b∈A→∀c∈ran⁡OcRb↔∀m∈dom⁡OO⁡mRb
60 53 59 bitr3d ⊢φ∧b∈A→∀c∈FTcRb↔∀m∈dom⁡OO⁡mRb
61 48 60 mtbid ⊢φ∧b∈A→¬∀m∈dom⁡OO⁡mRb
62 rexnal ⊢∃m∈dom⁡O¬O⁡mRb↔¬∀m∈dom⁡OO⁡mRb
63 61 62 sylibr ⊢φ∧b∈A→∃m∈dom⁡O¬O⁡mRb
64 1 2 3 4 5 6 7 ordtypelem7 ⊢φ∧b∈A∧m∈dom⁡O→O⁡mRb∨b∈ran⁡O
65 64 ord ⊢φ∧b∈A∧m∈dom⁡O→¬O⁡mRb→b∈ran⁡O
66 65 rexlimdva ⊢φ∧b∈A→∃m∈dom⁡O¬O⁡mRb→b∈ran⁡O
67 63 66 mpd ⊢φ∧b∈A→b∈ran⁡O
68 11 67 eqelssd ⊢φ→ran⁡O=A
69 isoeq5 ⊢ran⁡O=A→OIsomE,Rdom⁡Oran⁡O↔OIsomE,Rdom⁡OA
70 68 69 syl ⊢φ→OIsomE,Rdom⁡Oran⁡O↔OIsomE,Rdom⁡OA
71 9 70 mpbid ⊢φ→OIsomE,Rdom⁡OA