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 ⊢ 𝐹 = recs ( 𝐺 )
ordtypelem.2 ⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
ordtypelem.3 ⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
ordtypelem.5 ⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
ordtypelem.6 ⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
ordtypelem.7 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
ordtypelem.8 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
Assertion ordtypelem10 ( 𝜑 → 𝑂 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 1 2 3 4 5 6 7 ordtypelem8 ⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )
9 1 2 3 4 5 6 7 ordtypelem4 ⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
10 9 frnd ⊢ ( 𝜑 → ran 𝑂 ⊆ 𝐴 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑏 ∈ 𝐴 )
12 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑅 We 𝐴 )
13 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑅 Se 𝐴 )
14 9 ffund ⊢ ( 𝜑 → Fun 𝑂 )
15 14 funfnd ⊢ ( 𝜑 → 𝑂 Fn dom 𝑂 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑂 Fn dom 𝑂 )
17 1 2 3 4 5 12 13 ordtypelem8 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )
18 isof1o ⊢ ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) → 𝑂 : dom 𝑂 –1-1-onto→ ran 𝑂 )
19 f1of1 ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ran 𝑂 → 𝑂 : dom 𝑂 –1-1→ ran 𝑂 )
20 17 18 19 3syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑂 : dom 𝑂 –1-1→ ran 𝑂 )
21 simpl ⊢ ( ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) → 𝑏 ∈ 𝐴 )
22 seex ⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑏 ∈ 𝐴 ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 𝑅 𝑏 } ∈ V )
23 7 21 22 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → { 𝑐 ∈ 𝐴 ∣ 𝑐 𝑅 𝑏 } ∈ V )
24 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ran 𝑂 ⊆ 𝐴 )
25 rexnal ⊢ ( ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ↔ ¬ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 )
26 1 2 3 4 5 6 7 ordtypelem7 ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑚 ∈ dom 𝑂 ) → ( ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ∨ 𝑏 ∈ ran 𝑂 ) )
27 26 ord ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑚 ∈ dom 𝑂 ) → ( ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 → 𝑏 ∈ ran 𝑂 ) )
28 27 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 → 𝑏 ∈ ran 𝑂 ) )
29 25 28 syl5bir ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ¬ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 → 𝑏 ∈ ran 𝑂 ) )
30 29 con1d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ¬ 𝑏 ∈ ran 𝑂 → ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
31 30 impr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 )
32 breq1 ⊢ ( 𝑐 = ( 𝑂 ‘ 𝑚 ) → ( 𝑐 𝑅 𝑏 ↔ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
33 32 ralrn ⊢ ( 𝑂 Fn dom 𝑂 → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
34 16 33 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
35 31 34 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 )
36 ssrab ⊢ ( ran 𝑂 ⊆ { 𝑐 ∈ 𝐴 ∣ 𝑐 𝑅 𝑏 } ↔ ( ran 𝑂 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ) )
37 24 35 36 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ran 𝑂 ⊆ { 𝑐 ∈ 𝐴 ∣ 𝑐 𝑅 𝑏 } )
38 23 37 ssexd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ran 𝑂 ∈ V )
39 f1dmex ⊢ ( ( 𝑂 : dom 𝑂 –1-1→ ran 𝑂 ∧ ran 𝑂 ∈ V ) → dom 𝑂 ∈ V )
40 20 38 39 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → dom 𝑂 ∈ V )
41 16 40 fnexd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑂 ∈ V )
42 1 2 3 4 5 12 13 41 ordtypelem9 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )
43 isof1o ⊢ ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) → 𝑂 : dom 𝑂 –1-1-onto→ 𝐴 )
44 f1ofo ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ 𝐴 → 𝑂 : dom 𝑂 –onto→ 𝐴 )
45 forn ⊢ ( 𝑂 : dom 𝑂 –onto→ 𝐴 → ran 𝑂 = 𝐴 )
46 42 43 44 45 4syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → ran 𝑂 = 𝐴 )
47 11 46 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ran 𝑂 ) ) → 𝑏 ∈ ran 𝑂 )
48 47 expr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ¬ 𝑏 ∈ ran 𝑂 → 𝑏 ∈ ran 𝑂 ) )
49 48 pm2.18d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ ran 𝑂 )
50 10 49 eqelssd ⊢ ( 𝜑 → ran 𝑂 = 𝐴 )
51 isoeq5 ⊢ ( ran 𝑂 = 𝐴 → ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) ↔ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) )
52 50 51 syl ⊢ ( 𝜑 → ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) ↔ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) )
53 8 52 mpbid ⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )