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 A = f | x On f Fn x y x f y = F f y
Assertion tfrlem16 Lim dom recs F

Proof

Step Hyp Ref Expression
1 tfrlem.1 A = f | x On f Fn x y x f y = F f y
2 1 tfrlem8 Ord dom recs F
3 ordzsl Ord dom recs F dom recs F = z On dom recs F = suc z Lim dom recs F
4 2 3 mpbi dom recs F = z On dom recs F = suc z Lim dom recs F
5 res0 recs F =
6 0ex V
7 5 6 eqeltri recs F V
8 0elon On
9 1 tfrlem15 On dom recs F recs F V
10 8 9 ax-mp dom recs F recs F V
11 7 10 mpbir dom recs F
12 11 n0ii ¬ dom recs F =
13 12 pm2.21i dom recs F = Lim dom recs F
14 1 tfrlem13 ¬ recs F V
15 simpr z On dom recs F = suc z dom recs F = suc z
16 df-suc suc z = z z
17 15 16 eqtrdi z On dom recs F = suc z dom recs F = z z
18 17 reseq2d z On dom recs F = suc z recs F dom recs F = recs F z z
19 1 tfrlem6 Rel recs F
20 resdm Rel recs F recs F dom recs F = recs F
21 19 20 ax-mp recs F dom recs F = recs F
22 resundi recs F z z = recs F z recs F z
23 18 21 22 3eqtr3g z On dom recs F = suc z recs F = recs F z recs F z
24 vex z V
25 24 sucid z suc z
26 25 15 eleqtrrid z On dom recs F = suc z z dom recs F
27 1 tfrlem9a z dom recs F recs F z V
28 26 27 syl z On dom recs F = suc z recs F z V
29 snex z recs F z V
30 1 tfrlem7 Fun recs F
31 funressn Fun recs F recs F z z recs F z
32 30 31 ax-mp recs F z z recs F z
33 29 32 ssexi recs F z V
34 unexg recs F z V recs F z V recs F z recs F z V
35 28 33 34 sylancl z On dom recs F = suc z recs F z recs F z V
36 23 35 eqeltrd z On dom recs F = suc z recs F V
37 36 rexlimiva z On dom recs F = suc z recs F V
38 14 37 mto ¬ z On dom recs F = suc z
39 38 pm2.21i z On dom recs F = suc z Lim dom recs F
40 id Lim dom recs F Lim dom recs F
41 13 39 40 3jaoi dom recs F = z On dom recs F = suc z Lim dom recs F Lim dom recs F
42 4 41 ax-mp Lim dom recs F