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

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 𝑂 ⟶ 𝐴 ) )