This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtypelem6

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-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 ordtypelem6 ( ( 𝜑 ∧ 𝑀 ∈ 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 fveq2 ⊢ ( 𝑎 = 𝑁 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑁 ) )
9 8 breq1d ⊢ ( 𝑎 = 𝑁 → ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ( 𝐹 ‘ 𝑁 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
10 ssrab2 ⊢ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ⊆ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 }
11 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ dom 𝑂 )
12 1 2 3 4 5 6 7 ordtypelem4 ⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
13 12 fdmd ⊢ ( 𝜑 → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
15 11 14 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) )
16 1 2 3 4 5 6 7 ordtypelem3 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
17 15 16 syldan ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑣 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
18 10 17 sselid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝐹 ‘ 𝑀 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } )
19 breq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑀 ) → ( 𝑗 𝑅 𝑤 ↔ 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
20 19 ralbidv ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑀 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 ↔ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
21 20 elrab ⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } ↔ ( ( 𝐹 ‘ 𝑀 ) ∈ 𝐴 ∧ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
22 21 simprbi ⊢ ( ( 𝐹 ‘ 𝑀 ) ∈ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 𝑤 } → ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) )
23 18 22 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) )
24 1 tfr1a ⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 )
25 24 simpli ⊢ Fun 𝐹
26 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
27 25 26 mpbi ⊢ 𝐹 Fn dom 𝐹
28 24 simpri ⊢ Lim dom 𝐹
29 limord ⊢ ( Lim dom 𝐹 → Ord dom 𝐹 )
30 28 29 ax-mp ⊢ Ord dom 𝐹
31 inss2 ⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ dom 𝐹
32 13 31 eqsstrdi ⊢ ( 𝜑 → dom 𝑂 ⊆ dom 𝐹 )
33 32 sselda ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ dom 𝐹 )
34 ordelss ⊢ ( ( Ord dom 𝐹 ∧ 𝑀 ∈ dom 𝐹 ) → 𝑀 ⊆ dom 𝐹 )
35 30 33 34 sylancr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ⊆ dom 𝐹 )
36 breq1 ⊢ ( 𝑗 = ( 𝐹 ‘ 𝑎 ) → ( 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
37 36 ralima ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑀 ⊆ dom 𝐹 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
38 27 35 37 sylancr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( ∀ 𝑗 ∈ ( 𝐹 “ 𝑀 ) 𝑗 𝑅 ( 𝐹 ‘ 𝑀 ) ↔ ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) ) )
39 23 38 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) )
40 39 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ∀ 𝑎 ∈ 𝑀 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑀 ) )
41 simprr ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑁 ∈ 𝑀 )
42 9 40 41 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝐹 ‘ 𝑁 ) 𝑅 ( 𝐹 ‘ 𝑀 ) )
43 1 2 3 4 5 6 7 ordtypelem1 ⊢ ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
45 44 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑁 ) = ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑁 ) )
46 1 2 3 4 5 6 7 ordtypelem2 ⊢ ( 𝜑 → Ord 𝑇 )
47 inss1 ⊢ ( 𝑇 ∩ dom 𝐹 ) ⊆ 𝑇
48 13 47 eqsstrdi ⊢ ( 𝜑 → dom 𝑂 ⊆ 𝑇 )
49 48 sselda ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → 𝑀 ∈ 𝑇 )
50 49 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑀 ∈ 𝑇 )
51 ordelss ⊢ ( ( Ord 𝑇 ∧ 𝑀 ∈ 𝑇 ) → 𝑀 ⊆ 𝑇 )
52 46 50 51 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑀 ⊆ 𝑇 )
53 52 41 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → 𝑁 ∈ 𝑇 )
54 53 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
55 45 54 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
56 44 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑀 ) = ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑀 ) )
57 50 fvresd ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( ( 𝐹 ↾ 𝑇 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
58 56 57 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
59 42 55 58 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ dom 𝑂 ∧ 𝑁 ∈ 𝑀 ) ) → ( 𝑂 ‘ 𝑁 ) 𝑅 ( 𝑂 ‘ 𝑀 ) )
60 59 expr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ dom 𝑂 ) → ( 𝑁 ∈ 𝑀 → ( 𝑂 ‘ 𝑁 ) 𝑅 ( 𝑂 ‘ 𝑀 ) ) )