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 ⁡ h j R w
ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
ordtypelem.5 ⊢ T = x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
ordtypelem.6 ⊢ O = OrdIso R A
ordtypelem.7 ⊢ φ → R We A
ordtypelem.8 ⊢ φ → R Se A
ordtypelem9.1 ⊢ φ → O ∈ V
Assertion ordtypelem9 ⊢ φ → O Isom E , R dom ⁡ O A

Proof

Step Hyp Ref Expression
1 ordtypelem.1 ⊢ F = recs ⁡ G
2 ordtypelem.2 ⊢ C = w ∈ A | ∀ j ∈ ran ⁡ h j R w
3 ordtypelem.3 ⊢ G = h ∈ V ⟼ ι v ∈ C | ∀ u ∈ C ¬ u R v
4 ordtypelem.5 ⊢ T = x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t
5 ordtypelem.6 ⊢ O = OrdIso R A
6 ordtypelem.7 ⊢ φ → R We A
7 ordtypelem.8 ⊢ φ → R Se A
8 ordtypelem9.1 ⊢ φ → O ∈ V
9 1 2 3 4 5 6 7 ordtypelem8 ⊢ φ → O Isom E , R dom ⁡ O ran ⁡ 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 → F a = F T
28 27 raleqdv ⊢ a = T → ∀ c ∈ F a c R b ↔ ∀ c ∈ F T c R b
29 28 rexbidv ⊢ a = T → ∃ b ∈ A ∀ c ∈ F a c R b ↔ ∃ b ∈ A ∀ c ∈ F T c R b
30 breq1 ⊢ z = c → z R t ↔ c R t
31 30 cbvralvw ⊢ ∀ z ∈ F x z R t ↔ ∀ c ∈ F x c R t
32 breq2 ⊢ t = b → c R t ↔ c R b
33 32 ralbidv ⊢ t = b → ∀ c ∈ F x c R t ↔ ∀ c ∈ F x c R b
34 31 33 syl5bb ⊢ t = b → ∀ z ∈ F x z R t ↔ ∀ c ∈ F x c R b
35 34 cbvrexvw ⊢ ∃ t ∈ A ∀ z ∈ F x z R t ↔ ∃ b ∈ A ∀ c ∈ F x c R b
36 imaeq2 ⊢ x = a → F x = F a
37 36 raleqdv ⊢ x = a → ∀ c ∈ F x c R b ↔ ∀ c ∈ F a c R b
38 37 rexbidv ⊢ x = a → ∃ b ∈ A ∀ c ∈ F x c R b ↔ ∃ b ∈ A ∀ c ∈ F a c R b
39 35 38 syl5bb ⊢ x = a → ∃ t ∈ A ∀ z ∈ F x z R t ↔ ∃ b ∈ A ∀ c ∈ F a c R b
40 39 cbvrabv ⊢ x ∈ On | ∃ t ∈ A ∀ z ∈ F x z R t = a ∈ On | ∃ b ∈ A ∀ c ∈ F a c R b
41 4 40 eqtri ⊢ T = a ∈ On | ∃ b ∈ A ∀ c ∈ F a c R b
42 29 41 elrab2 ⊢ T ∈ T ↔ T ∈ On ∧ ∃ b ∈ A ∀ c ∈ F T c R b
43 42 baib ⊢ T ∈ On → T ∈ T ↔ ∃ b ∈ A ∀ c ∈ F T c R b
44 26 43 syl ⊢ φ → T ∈ T ↔ ∃ b ∈ A ∀ c ∈ F T c R b
45 14 44 mtbid ⊢ φ → ¬ ∃ b ∈ A ∀ c ∈ F T c R b
46 ralnex ⊢ ∀ b ∈ A ¬ ∀ c ∈ F T c R b ↔ ¬ ∃ b ∈ A ∀ c ∈ F T c R b
47 45 46 sylibr ⊢ φ → ∀ b ∈ A ¬ ∀ c ∈ F T c R b
48 47 r19.21bi ⊢ φ ∧ b ∈ A → ¬ ∀ c ∈ F T c R b
49 19 rneqd ⊢ φ → ran ⁡ O = ran ⁡ F ↾ T
50 df-ima ⊢ F T = ran ⁡ F ↾ T
51 49 50 eqtr4di ⊢ φ → ran ⁡ O = F T
52 51 adantr ⊢ φ ∧ b ∈ A → ran ⁡ O = F T
53 52 raleqdv ⊢ φ ∧ b ∈ A → ∀ c ∈ ran ⁡ O c R b ↔ ∀ c ∈ F T c R b
54 10 ffund ⊢ φ → Fun ⁡ O
55 54 funfnd ⊢ φ → O Fn dom ⁡ O
56 55 adantr ⊢ φ ∧ b ∈ A → O Fn dom ⁡ O
57 breq1 ⊢ c = O ⁡ m → c R b ↔ O ⁡ m R b
58 57 ralrn ⊢ O Fn dom ⁡ O → ∀ c ∈ ran ⁡ O c R b ↔ ∀ m ∈ dom ⁡ O O ⁡ m R b
59 56 58 syl ⊢ φ ∧ b ∈ A → ∀ c ∈ ran ⁡ O c R b ↔ ∀ m ∈ dom ⁡ O O ⁡ m R b
60 53 59 bitr3d ⊢ φ ∧ b ∈ A → ∀ c ∈ F T c R b ↔ ∀ m ∈ dom ⁡ O O ⁡ m R b
61 48 60 mtbid ⊢ φ ∧ b ∈ A → ¬ ∀ m ∈ dom ⁡ O O ⁡ m R b
62 rexnal ⊢ ∃ m ∈ dom ⁡ O ¬ O ⁡ m R b ↔ ¬ ∀ m ∈ dom ⁡ O O ⁡ m R b
63 61 62 sylibr ⊢ φ ∧ b ∈ A → ∃ m ∈ dom ⁡ O ¬ O ⁡ m R b
64 1 2 3 4 5 6 7 ordtypelem7 ⊢ φ ∧ b ∈ A ∧ m ∈ dom ⁡ O → O ⁡ m R b ∨ b ∈ ran ⁡ O
65 64 ord ⊢ φ ∧ b ∈ A ∧ m ∈ dom ⁡ O → ¬ O ⁡ m R b → b ∈ ran ⁡ O
66 65 rexlimdva ⊢ φ ∧ b ∈ A → ∃ m ∈ dom ⁡ O ¬ O ⁡ m R b → b ∈ ran ⁡ O
67 63 66 mpd ⊢ φ ∧ b ∈ A → b ∈ ran ⁡ O
68 11 67 eqelssd ⊢ φ → ran ⁡ O = A
69 isoeq5 ⊢ ran ⁡ O = A → O Isom E , R dom ⁡ O ran ⁡ O ↔ O Isom E , R dom ⁡ O A
70 68 69 syl ⊢ φ → O Isom E , R dom ⁡ O ran ⁡ O ↔ O Isom E , R dom ⁡ O A
71 9 70 mpbid ⊢ φ → O Isom E , R dom ⁡ O A