Metamath Proof Explorer

Theorem uzrdgfni

Description: The recursive definition generator on upper integers is a function. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 4-May-2015)

Ref Expression
Hypotheses om2uz.1 
|- C e. ZZ
om2uz.2 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
uzrdg.1 
|- A e. _V
uzrdg.2 
|- R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om )
uzrdg.3 
|- S = ran R
Assertion uzrdgfni 
|- S Fn ( ZZ>= ` C )

Proof

Step Hyp Ref Expression
1 om2uz.1 
 |-  C e. ZZ
2 om2uz.2 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3 uzrdg.1 
 |-  A e. _V
4 uzrdg.2 
 |-  R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om )
5 uzrdg.3 
 |-  S = ran R
6 5 eleq2i 
 |-  ( z e. S <-> z e. ran R )
7 frfnom 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om
8 4 fneq1i 
 |-  ( R Fn _om <-> ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om )
9 7 8 mpbir 
 |-  R Fn _om
10 fvelrnb 
 |-  ( R Fn _om -> ( z e. ran R <-> E. w e. _om ( R ` w ) = z ) )
11 9 10 ax-mp 
 |-  ( z e. ran R <-> E. w e. _om ( R ` w ) = z )
12 6 11 bitri 
 |-  ( z e. S <-> E. w e. _om ( R ` w ) = z )
13 1 2 3 4 om2uzrdg 
 |-  ( w e. _om -> ( R ` w ) = <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. )
14 1 2 om2uzuzi 
 |-  ( w e. _om -> ( G ` w ) e. ( ZZ>= ` C ) )
15 fvex 
 |-  ( 2nd ` ( R ` w ) ) e. _V
16 opelxpi 
 |-  ( ( ( G ` w ) e. ( ZZ>= ` C ) /\ ( 2nd ` ( R ` w ) ) e. _V ) -> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. e. ( ( ZZ>= ` C ) X. _V ) )
17 14 15 16 sylancl 
 |-  ( w e. _om -> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. e. ( ( ZZ>= ` C ) X. _V ) )
18 13 17 eqeltrd 
 |-  ( w e. _om -> ( R ` w ) e. ( ( ZZ>= ` C ) X. _V ) )
19 eleq1 
 |-  ( ( R ` w ) = z -> ( ( R ` w ) e. ( ( ZZ>= ` C ) X. _V ) <-> z e. ( ( ZZ>= ` C ) X. _V ) ) )
20 18 19 syl5ibcom 
 |-  ( w e. _om -> ( ( R ` w ) = z -> z e. ( ( ZZ>= ` C ) X. _V ) ) )
21 20 rexlimiv 
 |-  ( E. w e. _om ( R ` w ) = z -> z e. ( ( ZZ>= ` C ) X. _V ) )
22 12 21 sylbi 
 |-  ( z e. S -> z e. ( ( ZZ>= ` C ) X. _V ) )
23 22 ssriv 
 |-  S C_ ( ( ZZ>= ` C ) X. _V )
24 xpss 
 |-  ( ( ZZ>= ` C ) X. _V ) C_ ( _V X. _V )
25 23 24 sstri 
 |-  S C_ ( _V X. _V )
26 df-rel 
 |-  ( Rel S <-> S C_ ( _V X. _V ) )
27 25 26 mpbir 
 |-  Rel S
28 fvex 
 |-  ( 2nd ` ( R ` ( `' G ` v ) ) ) e. _V
29 eqeq2 
 |-  ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( z = w <-> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
30 29 imbi2d 
 |-  ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( ( <. v , z >. e. S -> z = w ) <-> ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) ) )
31 30 albidv 
 |-  ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( A. z ( <. v , z >. e. S -> z = w ) <-> A. z ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) ) )
32 28 31 spcev 
 |-  ( A. z ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) -> E. w A. z ( <. v , z >. e. S -> z = w ) )
33 5 eleq2i 
 |-  ( <. v , z >. e. S <-> <. v , z >. e. ran R )
34 fvelrnb 
 |-  ( R Fn _om -> ( <. v , z >. e. ran R <-> E. w e. _om ( R ` w ) = <. v , z >. ) )
35 9 34 ax-mp 
 |-  ( <. v , z >. e. ran R <-> E. w e. _om ( R ` w ) = <. v , z >. )
36 33 35 bitri 
 |-  ( <. v , z >. e. S <-> E. w e. _om ( R ` w ) = <. v , z >. )
37 13 eqeq1d 
 |-  ( w e. _om -> ( ( R ` w ) = <. v , z >. <-> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. ) )
38 fvex 
 |-  ( G ` w ) e. _V
39 38 15 opth1 
 |-  ( <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. -> ( G ` w ) = v )
40 37 39 syl6bi 
 |-  ( w e. _om -> ( ( R ` w ) = <. v , z >. -> ( G ` w ) = v ) )
41 1 2 om2uzf1oi 
 |-  G : _om -1-1-onto-> ( ZZ>= ` C )
42 f1ocnvfv 
 |-  ( ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ w e. _om ) -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
43 41 42 mpan 
 |-  ( w e. _om -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
44 40 43 syld 
 |-  ( w e. _om -> ( ( R ` w ) = <. v , z >. -> ( `' G ` v ) = w ) )
45 2fveq3 
 |-  ( ( `' G ` v ) = w -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) )
46 44 45 syl6 
 |-  ( w e. _om -> ( ( R ` w ) = <. v , z >. -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) ) )
47 46 imp 
 |-  ( ( w e. _om /\ ( R ` w ) = <. v , z >. ) -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) )
48 vex 
 |-  v e. _V
49 vex 
 |-  z e. _V
50 48 49 op2ndd 
 |-  ( ( R ` w ) = <. v , z >. -> ( 2nd ` ( R ` w ) ) = z )
51 50 adantl 
 |-  ( ( w e. _om /\ ( R ` w ) = <. v , z >. ) -> ( 2nd ` ( R ` w ) ) = z )
52 47 51 eqtr2d 
 |-  ( ( w e. _om /\ ( R ` w ) = <. v , z >. ) -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) )
53 52 rexlimiva 
 |-  ( E. w e. _om ( R ` w ) = <. v , z >. -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) )
54 36 53 sylbi 
 |-  ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) )
55 32 54 mpg 
 |-  E. w A. z ( <. v , z >. e. S -> z = w )
56 55 ax-gen 
 |-  A. v E. w A. z ( <. v , z >. e. S -> z = w )
57 dffun5 
 |-  ( Fun S <-> ( Rel S /\ A. v E. w A. z ( <. v , z >. e. S -> z = w ) ) )
58 27 56 57 mpbir2an 
 |-  Fun S
59 dmss 
 |-  ( S C_ ( ( ZZ>= ` C ) X. _V ) -> dom S C_ dom ( ( ZZ>= ` C ) X. _V ) )
60 23 59 ax-mp 
 |-  dom S C_ dom ( ( ZZ>= ` C ) X. _V )
61 dmxpss 
 |-  dom ( ( ZZ>= ` C ) X. _V ) C_ ( ZZ>= ` C )
62 60 61 sstri 
 |-  dom S C_ ( ZZ>= ` C )
63 1 2 3 4 uzrdglem 
 |-  ( v e. ( ZZ>= ` C ) -> <. v , ( 2nd ` ( R ` ( `' G ` v ) ) ) >. e. ran R )
64 63 5 eleqtrrdi 
 |-  ( v e. ( ZZ>= ` C ) -> <. v , ( 2nd ` ( R ` ( `' G ` v ) ) ) >. e. S )
65 48 28 opeldm 
 |-  ( <. v , ( 2nd ` ( R ` ( `' G ` v ) ) ) >. e. S -> v e. dom S )
66 64 65 syl 
 |-  ( v e. ( ZZ>= ` C ) -> v e. dom S )
67 66 ssriv 
 |-  ( ZZ>= ` C ) C_ dom S
68 62 67 eqssi 
 |-  dom S = ( ZZ>= ` C )
69 df-fn 
 |-  ( S Fn ( ZZ>= ` C ) <-> ( Fun S /\ dom S = ( ZZ>= ` C ) ) )
70 58 68 69 mpbir2an 
 |-  S Fn ( ZZ>= ` C )