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	sseldi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑇 ∩ 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 𝐹 ) ⟶ 𝐴 )