Metamath Proof Explorer


Theorem ordtypelem4

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 ordtypelem4 ( 𝜑𝑂 : ( 𝑇 ∩ 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 tfr1a ( Fun 𝐹 ∧ Lim dom 𝐹 )
9 8 simpli Fun 𝐹
10 funres ( Fun 𝐹 → Fun ( 𝐹𝑇 ) )
11 9 10 mp1i ( 𝜑 → Fun ( 𝐹𝑇 ) )
12 11 funfnd ( 𝜑 → ( 𝐹𝑇 ) Fn dom ( 𝐹𝑇 ) )
13 dmres dom ( 𝐹𝑇 ) = ( 𝑇 ∩ dom 𝐹 )
14 13 fneq2i ( ( 𝐹𝑇 ) Fn dom ( 𝐹𝑇 ) ↔ ( 𝐹𝑇 ) Fn ( 𝑇 ∩ dom 𝐹 ) )
15 12 14 sylib ( 𝜑 → ( 𝐹𝑇 ) Fn ( 𝑇 ∩ dom 𝐹 ) )
16 simpr ( ( 𝜑𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) )
17 16 elin1d ( ( 𝜑𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → 𝑎𝑇 )
18 17 fvresd ( ( 𝜑𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( ( 𝐹𝑇 ) ‘ 𝑎 ) = ( 𝐹𝑎 ) )
19 ssrab2 { 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ⊆ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 }
20 ssrab2 { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ⊆ 𝐴
21 19 20 sstri { 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } ⊆ 𝐴
22 1 2 3 4 5 6 7 ordtypelem3 ( ( 𝜑𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹𝑎 ) ∈ { 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ∣ ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ( 𝐹𝑎 ) 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 } )
23 21 22 sselid ( ( 𝜑𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( 𝐹𝑎 ) ∈ 𝐴 )
24 18 23 eqeltrd ( ( 𝜑𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ) → ( ( 𝐹𝑇 ) ‘ 𝑎 ) ∈ 𝐴 )
25 24 ralrimiva ( 𝜑 → ∀ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ( ( 𝐹𝑇 ) ‘ 𝑎 ) ∈ 𝐴 )
26 ffnfv ( ( 𝐹𝑇 ) : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ↔ ( ( 𝐹𝑇 ) Fn ( 𝑇 ∩ dom 𝐹 ) ∧ ∀ 𝑎 ∈ ( 𝑇 ∩ dom 𝐹 ) ( ( 𝐹𝑇 ) ‘ 𝑎 ) ∈ 𝐴 ) )
27 15 25 26 sylanbrc ( 𝜑 → ( 𝐹𝑇 ) : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
28 1 2 3 4 5 6 7 ordtypelem1 ( 𝜑𝑂 = ( 𝐹𝑇 ) )
29 28 feq1d ( 𝜑 → ( 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ↔ ( 𝐹𝑇 ) : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 ) )
30 27 29 mpbird ( 𝜑𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )