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 | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Assertion tfrlem16 
|- Lim dom recs ( F )

Proof

Step Hyp Ref Expression
1 tfrlem.1 
 |-  A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2 1 tfrlem8 
 |-  Ord dom recs ( F )
3 ordzsl 
 |-  ( Ord dom recs ( F ) <-> ( dom recs ( F ) = (/) \/ E. z e. On dom recs ( F ) = suc z \/ Lim dom recs ( F ) ) )
4 2 3 mpbi 
 |-  ( dom recs ( F ) = (/) \/ E. z e. On dom recs ( F ) = suc z \/ Lim dom recs ( F ) )
5 res0 
 |-  ( recs ( F ) |` (/) ) = (/)
6 0ex 
 |-  (/) e. _V
7 5 6 eqeltri 
 |-  ( recs ( F ) |` (/) ) e. _V
8 0elon 
 |-  (/) e. On
9 1 tfrlem15 
 |-  ( (/) e. On -> ( (/) e. dom recs ( F ) <-> ( recs ( F ) |` (/) ) e. _V ) )
10 8 9 ax-mp 
 |-  ( (/) e. dom recs ( F ) <-> ( recs ( F ) |` (/) ) e. _V )
11 7 10 mpbir 
 |-  (/) e. 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 ) e. _V
15 simpr 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> dom recs ( F ) = suc z )
16 df-suc 
 |-  suc z = ( z u. { z } )
17 15 16 eqtrdi 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> dom recs ( F ) = ( z u. { z } ) )
18 17 reseq2d 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> ( recs ( F ) |` dom recs ( F ) ) = ( recs ( F ) |` ( z u. { 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 u. { z } ) ) = ( ( recs ( F ) |` z ) u. ( recs ( F ) |` { z } ) )
23 18 21 22 3eqtr3g 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> recs ( F ) = ( ( recs ( F ) |` z ) u. ( recs ( F ) |` { z } ) ) )
24 vex 
 |-  z e. _V
25 24 sucid 
 |-  z e. suc z
26 25 15 eleqtrrid 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> z e. dom recs ( F ) )
27 1 tfrlem9a 
 |-  ( z e. dom recs ( F ) -> ( recs ( F ) |` z ) e. _V )
28 26 27 syl 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> ( recs ( F ) |` z ) e. _V )
29 snex 
 |-  { <. z , ( recs ( F ) ` z ) >. } e. _V
30 1 tfrlem7 
 |-  Fun recs ( F )
31 funressn 
 |-  ( Fun recs ( F ) -> ( recs ( F ) |` { z } ) C_ { <. z , ( recs ( F ) ` z ) >. } )
32 30 31 ax-mp 
 |-  ( recs ( F ) |` { z } ) C_ { <. z , ( recs ( F ) ` z ) >. }
33 29 32 ssexi 
 |-  ( recs ( F ) |` { z } ) e. _V
34 unexg 
 |-  ( ( ( recs ( F ) |` z ) e. _V /\ ( recs ( F ) |` { z } ) e. _V ) -> ( ( recs ( F ) |` z ) u. ( recs ( F ) |` { z } ) ) e. _V )
35 28 33 34 sylancl 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> ( ( recs ( F ) |` z ) u. ( recs ( F ) |` { z } ) ) e. _V )
36 23 35 eqeltrd 
 |-  ( ( z e. On /\ dom recs ( F ) = suc z ) -> recs ( F ) e. _V )
37 36 rexlimiva 
 |-  ( E. z e. On dom recs ( F ) = suc z -> recs ( F ) e. _V )
38 14 37 mto 
 |-  -. E. z e. On dom recs ( F ) = suc z
39 38 pm2.21i 
 |-  ( E. z e. 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 ) = (/) \/ E. z e. On dom recs ( F ) = suc z \/ Lim dom recs ( F ) ) -> Lim dom recs ( F ) )
42 4 41 ax-mp 
 |-  Lim dom recs ( F )