Theorem tfrlem16

Description: Lemma for finite recursion. Without assuming ax-rep , we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2	1	tfrlem8	⊢ Ord dom recs ( 𝐹 )
3		ordzsl	⊢ ( Ord dom recs ( 𝐹 ) ↔ ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) )
4	2 3	mpbi	⊢ ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) )
5		res0	⊢ ( recs ( 𝐹 ) ↾ ∅ ) = ∅
6		0ex	⊢ ∅ ∈ V
7	5 6	eqeltri	⊢ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V
8		0elon	⊢ ∅ ∈ On
9	1	tfrlem15	⊢ ( ∅ ∈ On → ( ∅ ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V ) )
10	8 9	ax-mp	⊢ ( ∅ ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V )
11	7 10	mpbir	⊢ ∅ ∈ dom recs ( 𝐹 )
12	11	n0ii	⊢ ¬ dom recs ( 𝐹 ) = ∅
13	12	pm2.21i	⊢ ( dom recs ( 𝐹 ) = ∅ → Lim dom recs ( 𝐹 ) )
14	1	tfrlem13	⊢ ¬ recs ( 𝐹 ) ∈ V
15		simpr	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → dom recs ( 𝐹 ) = suc 𝑧 )
16		df-suc	⊢ suc 𝑧 = ( 𝑧 ∪ { 𝑧 } )
17	15 16	eqtrdi	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → dom recs ( 𝐹 ) = ( 𝑧 ∪ { 𝑧 } ) )
18	17	reseq2d	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = ( recs ( 𝐹 ) ↾ ( 𝑧 ∪ { 𝑧 } ) ) )
19	1	tfrlem6	⊢ Rel recs ( 𝐹 )
20		resdm	⊢ ( Rel recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 ) )
21	19 20	ax-mp	⊢ ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 )
22		resundi	⊢ ( recs ( 𝐹 ) ↾ ( 𝑧 ∪ { 𝑧 } ) ) = ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) )
23	18 21 22	3eqtr3g	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → recs ( 𝐹 ) = ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) )
24		vex	⊢ 𝑧 ∈ V
25	24	sucid	⊢ 𝑧 ∈ suc 𝑧
26	25 15	eleqtrrid	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → 𝑧 ∈ dom recs ( 𝐹 ) )
27	1	tfrlem9a	⊢ ( 𝑧 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V )
28	26 27	syl	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V )
29		snex	⊢ { ⟨ 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) ⟩ } ∈ V
30	1	tfrlem7	⊢ Fun recs ( 𝐹 )
31		funressn	⊢ ( Fun recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) ⟩ } )
32	30 31	ax-mp	⊢ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) ⟩ }
33	29 32	ssexi	⊢ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ∈ V
34		unexg	⊢ ( ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V ∧ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ∈ V ) → ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ∈ V )
35	28 33 34	sylancl	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ∈ V )
36	23 35	eqeltrd	⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → recs ( 𝐹 ) ∈ V )
37	36	rexlimiva	⊢ ( ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 → recs ( 𝐹 ) ∈ V )
38	14 37	mto	⊢ ¬ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧
39	38	pm2.21i	⊢ ( ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 → Lim dom recs ( 𝐹 ) )
40		id	⊢ ( Lim dom recs ( 𝐹 ) → Lim dom recs ( 𝐹 ) )
41	13 39 40	3jaoi	⊢ ( ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) → Lim dom recs ( 𝐹 ) )
42	4 41	ax-mp	⊢ Lim dom recs ( 𝐹 )