Theorem tfrlem8

Description: Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994) (Proof shortened by Alan Sare, 11-Mar-2008)

	Ref	Expression
Hypothesis	tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
Assertion	tfrlem8	⊢ Ord dom recs ( 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2	1	tfrlem3	⊢ 𝐴 = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }
3	2	eqabri	⊢ ( 𝑔 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) )
4		fndm	⊢ ( 𝑔 Fn 𝑧 → dom 𝑔 = 𝑧 )
5	4	adantr	⊢ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → dom 𝑔 = 𝑧 )
6	5	eleq1d	⊢ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → ( dom 𝑔 ∈ On ↔ 𝑧 ∈ On ) )
7	6	biimprcd	⊢ ( 𝑧 ∈ On → ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → dom 𝑔 ∈ On ) )
8	7	rexlimiv	⊢ ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → dom 𝑔 ∈ On )
9	3 8	sylbi	⊢ ( 𝑔 ∈ 𝐴 → dom 𝑔 ∈ On )
10		eleq1a	⊢ ( dom 𝑔 ∈ On → ( 𝑧 = dom 𝑔 → 𝑧 ∈ On ) )
11	9 10	syl	⊢ ( 𝑔 ∈ 𝐴 → ( 𝑧 = dom 𝑔 → 𝑧 ∈ On ) )
12	11	rexlimiv	⊢ ( ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 → 𝑧 ∈ On )
13	12	abssi	⊢ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } ⊆ On
14		ssorduni	⊢ ( { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } ⊆ On → Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } )
15	13 14	ax-mp	⊢ Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 }
16	1	recsfval	⊢ recs ( 𝐹 ) = ∪ 𝐴
17	16	dmeqi	⊢ dom recs ( 𝐹 ) = dom ∪ 𝐴
18		dmuni	⊢ dom ∪ 𝐴 = ∪ 𝑔 ∈ 𝐴 dom 𝑔
19		vex	⊢ 𝑔 ∈ V
20	19	dmex	⊢ dom 𝑔 ∈ V
21	20	dfiun2	⊢ ∪ 𝑔 ∈ 𝐴 dom 𝑔 = ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 }
22	17 18 21	3eqtri	⊢ dom recs ( 𝐹 ) = ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 }
23		ordeq	⊢ ( dom recs ( 𝐹 ) = ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } → ( Ord dom recs ( 𝐹 ) ↔ Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } ) )
24	22 23	ax-mp	⊢ ( Ord dom recs ( 𝐹 ) ↔ Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } )
25	15 24	mpbir	⊢ Ord dom recs ( 𝐹 )