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