This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )