Metamath Proof Explorer

Theorem uzrdglem

Description: A helper lemma for the value of a recursive definition generator on upper integers. (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 )
	Assertion	uzrdglem	\|- ( B e. ( ZZ>= ` C ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. ran R )

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	1 2	om2uzf1oi	\|- G : _om -1-1-onto-> ( ZZ>= ` C )
6		f1ocnvdm	\|- ( ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ B e. ( ZZ>= ` C ) ) -> ( `' G ` B ) e. _om )
7	5 6	mpan	\|- ( B e. ( ZZ>= ` C ) -> ( `' G ` B ) e. _om )
8	1 2 3 4	om2uzrdg	\|- ( ( `' G ` B ) e. _om -> ( R ` ( `' G ` B ) ) = <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
9	7 8	syl	\|- ( B e. ( ZZ>= ` C ) -> ( R ` ( `' G ` B ) ) = <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
10		f1ocnvfv2	\|- ( ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ B e. ( ZZ>= ` C ) ) -> ( G ` ( `' G ` B ) ) = B )
11	5 10	mpan	\|- ( B e. ( ZZ>= ` C ) -> ( G ` ( `' G ` B ) ) = B )
12	11	opeq1d	\|- ( B e. ( ZZ>= ` C ) -> <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. = <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
13	9 12	eqtrd	\|- ( B e. ( ZZ>= ` C ) -> ( R ` ( `' G ` B ) ) = <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
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		fnfvelrn	\|- ( ( R Fn _om /\ ( `' G ` B ) e. _om ) -> ( R ` ( `' G ` B ) ) e. ran R )
18	16 7 17	sylancr	\|- ( B e. ( ZZ>= ` C ) -> ( R ` ( `' G ` B ) ) e. ran R )
19	13 18	eqeltrrd	\|- ( B e. ( ZZ>= ` C ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. ran R )