Theorem uzrdg0i

Description: Initial value of a recursive definition generator on upper integers. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 18-Nov-2014)

	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	uzrdg0i	|- ( S ` C ) = A

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	1 2 3 4 5	uzrdgfni	|- S Fn ( ZZ>= ` C )
7		fnfun	|- ( S Fn ( ZZ>= ` C ) -> Fun S )
8	6 7	ax-mp	|- Fun S
9	4	fveq1i	|- ( R ` (/) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) )
10		opex	|- <. C , A >. e. _V
11		fr0g	|- ( <. C , A >. e. _V -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >. )
12	10 11	ax-mp	|- ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >.
13	9 12	eqtri	|- ( R ` (/) ) = <. C , A >.
14		frfnom	|- ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om
15	4	fneq1i	|- ( R Fn _om <-> ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om )
16	14 15	mpbir	|- R Fn _om
17		peano1	|- (/) e. _om
18		fnfvelrn	|- ( ( R Fn _om /\ (/) e. _om ) -> ( R ` (/) ) e. ran R )
19	16 17 18	mp2an	|- ( R ` (/) ) e. ran R
20	13 19	eqeltrri	|- <. C , A >. e. ran R
21	20 5	eleqtrri	|- <. C , A >. e. S
22		funopfv	|- ( Fun S -> ( <. C , A >. e. S -> ( S ` C ) = A ) )
23	8 21 22	mp2	|- ( S ` C ) = A