Metamath Proof Explorer

Theorem noseqrdglem

Description: A helper lemma for the value of a recursive defintion generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 
|- ( ph -> C e. No )
om2noseq.2 
|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
om2noseq.3 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
noseqrdg.1 
|- ( ph -> A e. V )
noseqrdg.2 
|- ( ph -> R = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) )
Assertion noseqrdglem 
|- ( ( ph /\ B e. Z ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. ran R )

Proof

Step Hyp Ref Expression
1 om2noseq.1 
 |-  ( ph -> C e. No )
2 om2noseq.2 
 |-  ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
3 om2noseq.3 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
4 noseqrdg.1 
 |-  ( ph -> A e. V )
5 noseqrdg.2 
 |-  ( ph -> R = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) )
6 1 2 3 om2noseqf1o 
 |-  ( ph -> G : _om -1-1-onto-> Z )
7 f1ocnvdm 
 |-  ( ( G : _om -1-1-onto-> Z /\ B e. Z ) -> ( `' G ` B ) e. _om )
8 6 7 sylan 
 |-  ( ( ph /\ B e. Z ) -> ( `' G ` B ) e. _om )
9 1 2 3 4 5 om2noseqrdg 
 |-  ( ( ph /\ ( `' G ` B ) e. _om ) -> ( R ` ( `' G ` B ) ) = <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
10 8 9 syldan 
 |-  ( ( ph /\ B e. Z ) -> ( R ` ( `' G ` B ) ) = <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
11 f1ocnvfv2 
 |-  ( ( G : _om -1-1-onto-> Z /\ B e. Z ) -> ( G ` ( `' G ` B ) ) = B )
12 6 11 sylan 
 |-  ( ( ph /\ B e. Z ) -> ( G ` ( `' G ` B ) ) = B )
13 12 opeq1d 
 |-  ( ( ph /\ B e. Z ) -> <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. = <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
14 10 13 eqtrd 
 |-  ( ( ph /\ B e. Z ) -> ( R ` ( `' G ` B ) ) = <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
15 frfnom 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om
16 5 fneq1d 
 |-  ( ph -> ( R Fn _om <-> ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om ) )
17 15 16 mpbiri 
 |-  ( ph -> R Fn _om )
18 17 adantr 
 |-  ( ( ph /\ B e. Z ) -> R Fn _om )
19 18 8 fnfvelrnd 
 |-  ( ( ph /\ B e. Z ) -> ( R ` ( `' G ` B ) ) e. ran R )
20 14 19 eqeltrrd 
 |-  ( ( ph /\ B e. Z ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. ran R )