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 𝐹 = recs ( 𝐺 )
ordtypelem.2 𝐶 = { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
ordtypelem.3 𝐺 = ( ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) )
ordtypelem.5 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 }
ordtypelem.6 𝑂 = OrdIso ( 𝑅 , 𝐴 )
ordtypelem.7 ( 𝜑𝑅 We 𝐴 )
ordtypelem.8 ( 𝜑𝑅 Se 𝐴 )
ordtypelem9.1 ( 𝜑𝑂𝑉 )
Assertion ordtypelem9 ( 𝜑𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ordtypelem.1 𝐹 = recs ( 𝐺 )
2 ordtypelem.2 𝐶 = { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
3 ordtypelem.3 𝐺 = ( ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4 ordtypelem.5 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 }
5 ordtypelem.6 𝑂 = OrdIso ( 𝑅 , 𝐴 )
6 ordtypelem.7 ( 𝜑𝑅 We 𝐴 )
7 ordtypelem.8 ( 𝜑𝑅 Se 𝐴 )
8 ordtypelem9.1 ( 𝜑𝑂𝑉 )
9 1 2 3 4 5 6 7 ordtypelem8 ( 𝜑𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )
10 1 2 3 4 5 6 7 ordtypelem4 ( 𝜑𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
11 10 frnd ( 𝜑 → ran 𝑂𝐴 )
12 1 2 3 4 5 6 7 ordtypelem2 ( 𝜑 → Ord 𝑇 )
13 ordirr ( Ord 𝑇 → ¬ 𝑇𝑇 )
14 12 13 syl ( 𝜑 → ¬ 𝑇𝑇 )
15 1 tfr1a ( Fun 𝐹 ∧ Lim dom 𝐹 )
16 15 simpri Lim dom 𝐹
17 limord ( Lim dom 𝐹 → Ord dom 𝐹 )
18 16 17 ax-mp Ord dom 𝐹
19 1 2 3 4 5 6 7 ordtypelem1 ( 𝜑𝑂 = ( 𝐹𝑇 ) )
20 8 elexd ( 𝜑𝑂 ∈ V )
21 19 20 eqeltrrd ( 𝜑 → ( 𝐹𝑇 ) ∈ V )
22 1 tfr2b ( Ord 𝑇 → ( 𝑇 ∈ dom 𝐹 ↔ ( 𝐹𝑇 ) ∈ V ) )
23 12 22 syl ( 𝜑 → ( 𝑇 ∈ dom 𝐹 ↔ ( 𝐹𝑇 ) ∈ V ) )
24 21 23 mpbird ( 𝜑𝑇 ∈ dom 𝐹 )
25 ordelon ( ( Ord dom 𝐹𝑇 ∈ dom 𝐹 ) → 𝑇 ∈ On )
26 18 24 25 sylancr ( 𝜑𝑇 ∈ On )
27 imaeq2 ( 𝑎 = 𝑇 → ( 𝐹𝑎 ) = ( 𝐹𝑇 ) )
28 27 raleqdv ( 𝑎 = 𝑇 → ( ∀ 𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ) )
29 28 rexbidv ( 𝑎 = 𝑇 → ( ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 ↔ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ) )
30 breq1 ( 𝑧 = 𝑐 → ( 𝑧 𝑅 𝑡𝑐 𝑅 𝑡 ) )
31 30 cbvralvw ( ∀ 𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑡 )
32 breq2 ( 𝑡 = 𝑏 → ( 𝑐 𝑅 𝑡𝑐 𝑅 𝑏 ) )
33 32 ralbidv ( 𝑡 = 𝑏 → ( ∀ 𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑡 ↔ ∀ 𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑏 ) )
34 31 33 syl5bb ( 𝑡 = 𝑏 → ( ∀ 𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑏 ) )
35 34 cbvrexvw ( ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑏 )
36 imaeq2 ( 𝑥 = 𝑎 → ( 𝐹𝑥 ) = ( 𝐹𝑎 ) )
37 36 raleqdv ( 𝑥 = 𝑎 → ( ∀ 𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 ) )
38 37 rexbidv ( 𝑥 = 𝑎 → ( ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑥 ) 𝑐 𝑅 𝑏 ↔ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 ) )
39 35 38 syl5bb ( 𝑥 = 𝑎 → ( ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 ) )
40 39 cbvrabv { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( 𝐹𝑥 ) 𝑧 𝑅 𝑡 } = { 𝑎 ∈ On ∣ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 }
41 4 40 eqtri 𝑇 = { 𝑎 ∈ On ∣ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑎 ) 𝑐 𝑅 𝑏 }
42 29 41 elrab2 ( 𝑇𝑇 ↔ ( 𝑇 ∈ On ∧ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ) )
43 42 baib ( 𝑇 ∈ On → ( 𝑇𝑇 ↔ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ) )
44 26 43 syl ( 𝜑 → ( 𝑇𝑇 ↔ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ) )
45 14 44 mtbid ( 𝜑 → ¬ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 )
46 ralnex ( ∀ 𝑏𝐴 ¬ ∀ 𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ↔ ¬ ∃ 𝑏𝐴𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 )
47 45 46 sylibr ( 𝜑 → ∀ 𝑏𝐴 ¬ ∀ 𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 )
48 47 r19.21bi ( ( 𝜑𝑏𝐴 ) → ¬ ∀ 𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 )
49 19 rneqd ( 𝜑 → ran 𝑂 = ran ( 𝐹𝑇 ) )
50 df-ima ( 𝐹𝑇 ) = ran ( 𝐹𝑇 )
51 49 50 eqtr4di ( 𝜑 → ran 𝑂 = ( 𝐹𝑇 ) )
52 51 adantr ( ( 𝜑𝑏𝐴 ) → ran 𝑂 = ( 𝐹𝑇 ) )
53 52 raleqdv ( ( 𝜑𝑏𝐴 ) → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ) )
54 10 ffund ( 𝜑 → Fun 𝑂 )
55 54 funfnd ( 𝜑𝑂 Fn dom 𝑂 )
56 55 adantr ( ( 𝜑𝑏𝐴 ) → 𝑂 Fn dom 𝑂 )
57 breq1 ( 𝑐 = ( 𝑂𝑚 ) → ( 𝑐 𝑅 𝑏 ↔ ( 𝑂𝑚 ) 𝑅 𝑏 ) )
58 57 ralrn ( 𝑂 Fn dom 𝑂 → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂𝑚 ) 𝑅 𝑏 ) )
59 56 58 syl ( ( 𝜑𝑏𝐴 ) → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂𝑚 ) 𝑅 𝑏 ) )
60 53 59 bitr3d ( ( 𝜑𝑏𝐴 ) → ( ∀ 𝑐 ∈ ( 𝐹𝑇 ) 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂𝑚 ) 𝑅 𝑏 ) )
61 48 60 mtbid ( ( 𝜑𝑏𝐴 ) → ¬ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂𝑚 ) 𝑅 𝑏 )
62 rexnal ( ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂𝑚 ) 𝑅 𝑏 ↔ ¬ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂𝑚 ) 𝑅 𝑏 )
63 61 62 sylibr ( ( 𝜑𝑏𝐴 ) → ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂𝑚 ) 𝑅 𝑏 )
64 1 2 3 4 5 6 7 ordtypelem7 ( ( ( 𝜑𝑏𝐴 ) ∧ 𝑚 ∈ dom 𝑂 ) → ( ( 𝑂𝑚 ) 𝑅 𝑏𝑏 ∈ ran 𝑂 ) )
65 64 ord ( ( ( 𝜑𝑏𝐴 ) ∧ 𝑚 ∈ dom 𝑂 ) → ( ¬ ( 𝑂𝑚 ) 𝑅 𝑏𝑏 ∈ ran 𝑂 ) )
66 65 rexlimdva ( ( 𝜑𝑏𝐴 ) → ( ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂𝑚 ) 𝑅 𝑏𝑏 ∈ ran 𝑂 ) )
67 63 66 mpd ( ( 𝜑𝑏𝐴 ) → 𝑏 ∈ ran 𝑂 )
68 11 67 eqelssd ( 𝜑 → ran 𝑂 = 𝐴 )
69 isoeq5 ( ran 𝑂 = 𝐴 → ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) ↔ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) )
70 68 69 syl ( 𝜑 → ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) ↔ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) )
71 9 70 mpbid ( 𝜑𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )