Metamath Proof Explorer


Theorem ordtypelem5

Description: Lemma for ordtype . (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 ordtypelem5 ( 𝜑 → ( Ord dom 𝑂𝑂 : 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 ordtypelem2 ( 𝜑 → Ord 𝑇 )
9 1 tfr1a ( Fun 𝐹 ∧ Lim dom 𝐹 )
10 9 simpri Lim dom 𝐹
11 limord ( Lim dom 𝐹 → Ord dom 𝐹 )
12 10 11 ax-mp Ord dom 𝐹
13 ordin ( ( Ord 𝑇 ∧ Ord dom 𝐹 ) → Ord ( 𝑇 ∩ dom 𝐹 ) )
14 8 12 13 sylancl ( 𝜑 → Ord ( 𝑇 ∩ dom 𝐹 ) )
15 1 2 3 4 5 6 7 ordtypelem4 ( 𝜑𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
16 15 fdmd ( 𝜑 → dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) )
17 ordeq ( dom 𝑂 = ( 𝑇 ∩ dom 𝐹 ) → ( Ord dom 𝑂 ↔ Ord ( 𝑇 ∩ dom 𝐹 ) ) )
18 16 17 syl ( 𝜑 → ( Ord dom 𝑂 ↔ Ord ( 𝑇 ∩ dom 𝐹 ) ) )
19 14 18 mpbird ( 𝜑 → Ord dom 𝑂 )
20 15 ffdmd ( 𝜑𝑂 : dom 𝑂𝐴 )
21 19 20 jca ( 𝜑 → ( Ord dom 𝑂𝑂 : dom 𝑂𝐴 ) )