Metamath Proof Explorer

Theorem noseqrdg0

Description: Initial value of a recursive definition 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 ) )
noseqrdg.3 
|- ( ph -> S = ran R )
Assertion noseqrdg0 
|- ( ph -> ( S ` C ) = A )

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 noseqrdg.3 
 |-  ( ph -> S = ran R )
7 1 2 3 4 5 6 noseqrdgfn 
 |-  ( ph -> S Fn Z )
8 7 fnfund 
 |-  ( ph -> Fun S )
9 frfnom 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om
10 5 fneq1d 
 |-  ( ph -> ( R Fn _om <-> ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om ) )
11 9 10 mpbiri 
 |-  ( ph -> R Fn _om )
12 peano1 
 |-  (/) e. _om
13 fnfvelrn 
 |-  ( ( R Fn _om /\ (/) e. _om ) -> ( R ` (/) ) e. ran R )
14 11 12 13 sylancl 
 |-  ( ph -> ( R ` (/) ) e. ran R )
15 5 fveq1d 
 |-  ( ph -> ( R ` (/) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) )
16 opex 
 |-  <. C , A >. e. _V
17 fr0g 
 |-  ( <. C , A >. e. _V -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >. )
18 16 17 ax-mp 
 |-  ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >.
19 15 18 eqtr2di 
 |-  ( ph -> <. C , A >. = ( R ` (/) ) )
20 14 19 6 3eltr4d 
 |-  ( ph -> <. C , A >. e. S )
21 funopfv 
 |-  ( Fun S -> ( <. C , A >. e. S -> ( S ` C ) = A ) )
22 8 20 21 sylc 
 |-  ( ph -> ( S ` C ) = A )