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

Metamath Proof Explorer

Theorem uzrdg0i

Proof