Metamath Proof Explorer

Theorem ordtypelem10

Description: Lemma for ordtype . Using ax-rep , exclude the possibility that O is a proper class and does not enumerate all of A . (Contributed by Mario Carneiro, 25-Jun-2015)

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
Assertion ordtypelem10 ⊢ φ → 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 1 2 3 4 5 6 7 ordtypelem8 ⊢ φ → O Isom E , R dom ⁡ O ran ⁡ O
9 1 2 3 4 5 6 7 ordtypelem4 ⊢ φ → O : T ∩ dom ⁡ F ⟶ A
10 9 frnd ⊢ φ → ran ⁡ O ⊆ A
11 simprl ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → b ∈ A
12 6 adantr ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → R We A
13 7 adantr ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → R Se A
14 9 ffund ⊢ φ → Fun ⁡ O
15 14 funfnd ⊢ φ → O Fn dom ⁡ O
16 15 adantr ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → O Fn dom ⁡ O
17 1 2 3 4 5 12 13 ordtypelem8 ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → O Isom E , R dom ⁡ O ran ⁡ O
18 isof1o ⊢ O Isom E , R dom ⁡ O ran ⁡ O → O : dom ⁡ O ⟶ 1-1 onto ran ⁡ O
19 f1of1 ⊢ O : dom ⁡ O ⟶ 1-1 onto ran ⁡ O → O : dom ⁡ O ⟶ 1-1 ran ⁡ O
20 17 18 19 3syl ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → O : dom ⁡ O ⟶ 1-1 ran ⁡ O
21 simpl ⊢ b ∈ A ∧ ¬ b ∈ ran ⁡ O → b ∈ A
22 seex ⊢ R Se A ∧ b ∈ A → c ∈ A | c R b ∈ V
23 7 21 22 syl2an ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → c ∈ A | c R b ∈ V
24 10 adantr ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ran ⁡ O ⊆ A
25 rexnal ⊢ ∃ m ∈ dom ⁡ O ¬ O ⁡ m R b ↔ ¬ ∀ m ∈ dom ⁡ O O ⁡ m R b
26 1 2 3 4 5 6 7 ordtypelem7 ⊢ φ ∧ b ∈ A ∧ m ∈ dom ⁡ O → O ⁡ m R b ∨ b ∈ ran ⁡ O
27 26 ord ⊢ φ ∧ b ∈ A ∧ m ∈ dom ⁡ O → ¬ O ⁡ m R b → b ∈ ran ⁡ O
28 27 rexlimdva ⊢ φ ∧ b ∈ A → ∃ m ∈ dom ⁡ O ¬ O ⁡ m R b → b ∈ ran ⁡ O
29 25 28 syl5bir ⊢ φ ∧ b ∈ A → ¬ ∀ m ∈ dom ⁡ O O ⁡ m R b → b ∈ ran ⁡ O
30 29 con1d ⊢ φ ∧ b ∈ A → ¬ b ∈ ran ⁡ O → ∀ m ∈ dom ⁡ O O ⁡ m R b
31 30 impr ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ∀ m ∈ dom ⁡ O O ⁡ m R b
32 breq1 ⊢ c = O ⁡ m → c R b ↔ O ⁡ m R b
33 32 ralrn ⊢ O Fn dom ⁡ O → ∀ c ∈ ran ⁡ O c R b ↔ ∀ m ∈ dom ⁡ O O ⁡ m R b
34 16 33 syl ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ∀ c ∈ ran ⁡ O c R b ↔ ∀ m ∈ dom ⁡ O O ⁡ m R b
35 31 34 mpbird ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ∀ c ∈ ran ⁡ O c R b
36 ssrab ⊢ ran ⁡ O ⊆ c ∈ A | c R b ↔ ran ⁡ O ⊆ A ∧ ∀ c ∈ ran ⁡ O c R b
37 24 35 36 sylanbrc ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ran ⁡ O ⊆ c ∈ A | c R b
38 23 37 ssexd ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ran ⁡ O ∈ V
39 f1dmex ⊢ O : dom ⁡ O ⟶ 1-1 ran ⁡ O ∧ ran ⁡ O ∈ V → dom ⁡ O ∈ V
40 20 38 39 syl2anc ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → dom ⁡ O ∈ V
41 16 40 fnexd ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → O ∈ V
42 1 2 3 4 5 12 13 41 ordtypelem9 ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → O Isom E , R dom ⁡ O A
43 isof1o ⊢ O Isom E , R dom ⁡ O A → O : dom ⁡ O ⟶ 1-1 onto A
44 f1ofo ⊢ O : dom ⁡ O ⟶ 1-1 onto A → O : dom ⁡ O ⟶ onto A
45 forn ⊢ O : dom ⁡ O ⟶ onto A → ran ⁡ O = A
46 42 43 44 45 4syl ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → ran ⁡ O = A
47 11 46 eleqtrrd ⊢ φ ∧ b ∈ A ∧ ¬ b ∈ ran ⁡ O → b ∈ ran ⁡ O
48 47 expr ⊢ φ ∧ b ∈ A → ¬ b ∈ ran ⁡ O → b ∈ ran ⁡ O
49 48 pm2.18d ⊢ φ ∧ b ∈ A → b ∈ ran ⁡ O
50 10 49 eqelssd ⊢ φ → ran ⁡ O = A
51 isoeq5 ⊢ ran ⁡ O = A → O Isom E , R dom ⁡ O ran ⁡ O ↔ O Isom E , R dom ⁡ O A
52 50 51 syl ⊢ φ → O Isom E , R dom ⁡ O ran ⁡ O ↔ O Isom E , R dom ⁡ O A
53 8 52 mpbid ⊢ φ → O Isom E , R dom ⁡ O A