Metamath Proof Explorer


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 ( 𝐹 )