Metamath Proof Explorer

Theorem noseqrdgfn

Description: The recursive definition generator on surreal sequences is a function. (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 noseqrdgfn 
|- ( ph -> S Fn Z )

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 6 eleq2d 
 |-  ( ph -> ( z e. S <-> z e. ran R ) )
8 frfnom 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om
9 5 fneq1d 
 |-  ( ph -> ( R Fn _om <-> ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) Fn _om ) )
10 8 9 mpbiri 
 |-  ( ph -> R Fn _om )
11 fvelrnb 
 |-  ( R Fn _om -> ( z e. ran R <-> E. w e. _om ( R ` w ) = z ) )
12 10 11 syl 
 |-  ( ph -> ( z e. ran R <-> E. w e. _om ( R ` w ) = z ) )
13 7 12 bitrd 
 |-  ( ph -> ( z e. S <-> E. w e. _om ( R ` w ) = z ) )
14 1 2 3 4 5 om2noseqrdg 
 |-  ( ( ph /\ w e. _om ) -> ( R ` w ) = <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. )
15 1 2 3 om2noseqfo 
 |-  ( ph -> G : _om -onto-> Z )
16 fof 
 |-  ( G : _om -onto-> Z -> G : _om --> Z )
17 15 16 syl 
 |-  ( ph -> G : _om --> Z )
18 17 ffvelcdmda 
 |-  ( ( ph /\ w e. _om ) -> ( G ` w ) e. Z )
19 fvex 
 |-  ( 2nd ` ( R ` w ) ) e. _V
20 opelxpi 
 |-  ( ( ( G ` w ) e. Z /\ ( 2nd ` ( R ` w ) ) e. _V ) -> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. e. ( Z X. _V ) )
21 18 19 20 sylancl 
 |-  ( ( ph /\ w e. _om ) -> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. e. ( Z X. _V ) )
22 14 21 eqeltrd 
 |-  ( ( ph /\ w e. _om ) -> ( R ` w ) e. ( Z X. _V ) )
23 eleq1 
 |-  ( ( R ` w ) = z -> ( ( R ` w ) e. ( Z X. _V ) <-> z e. ( Z X. _V ) ) )
24 22 23 syl5ibcom 
 |-  ( ( ph /\ w e. _om ) -> ( ( R ` w ) = z -> z e. ( Z X. _V ) ) )
25 24 rexlimdva 
 |-  ( ph -> ( E. w e. _om ( R ` w ) = z -> z e. ( Z X. _V ) ) )
26 13 25 sylbid 
 |-  ( ph -> ( z e. S -> z e. ( Z X. _V ) ) )
27 26 ssrdv 
 |-  ( ph -> S C_ ( Z X. _V ) )
28 relxp 
 |-  Rel ( Z X. _V )
29 relss 
 |-  ( S C_ ( Z X. _V ) -> ( Rel ( Z X. _V ) -> Rel S ) )
30 27 28 29 mpisyl 
 |-  ( ph -> Rel S )
31 6 eleq2d 
 |-  ( ph -> ( <. v , z >. e. S <-> <. v , z >. e. ran R ) )
32 fvelrnb 
 |-  ( R Fn _om -> ( <. v , z >. e. ran R <-> E. w e. _om ( R ` w ) = <. v , z >. ) )
33 10 32 syl 
 |-  ( ph -> ( <. v , z >. e. ran R <-> E. w e. _om ( R ` w ) = <. v , z >. ) )
34 31 33 bitrd 
 |-  ( ph -> ( <. v , z >. e. S <-> E. w e. _om ( R ` w ) = <. v , z >. ) )
35 14 eqeq1d 
 |-  ( ( ph /\ w e. _om ) -> ( ( R ` w ) = <. v , z >. <-> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. ) )
36 35 biimpd 
 |-  ( ( ph /\ w e. _om ) -> ( ( R ` w ) = <. v , z >. -> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. ) )
37 36 impr 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. )
38 fvex 
 |-  ( G ` w ) e. _V
39 38 19 opth1 
 |-  ( <. ( G ` w ) , ( 2nd ` ( R ` w ) ) >. = <. v , z >. -> ( G ` w ) = v )
40 37 39 syl 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> ( G ` w ) = v )
41 1 2 3 om2noseqf1o 
 |-  ( ph -> G : _om -1-1-onto-> Z )
42 f1ocnvfv 
 |-  ( ( G : _om -1-1-onto-> Z /\ w e. _om ) -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
43 41 42 sylan 
 |-  ( ( ph /\ w e. _om ) -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
44 43 adantrr 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> ( ( G ` w ) = v -> ( `' G ` v ) = w ) )
45 40 44 mpd 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> ( `' G ` v ) = w )
46 45 fveq2d 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> ( R ` ( `' G ` v ) ) = ( R ` w ) )
47 46 fveq2d 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> ( 2nd ` ( R ` ( `' G ` v ) ) ) = ( 2nd ` ( R ` w ) ) )
48 vex 
 |-  v e. _V
49 vex 
 |-  z e. _V
50 48 49 op2ndd 
 |-  ( ( R ` w ) = <. v , z >. -> ( 2nd ` ( R ` w ) ) = z )
51 50 ad2antll 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> ( 2nd ` ( R ` w ) ) = z )
52 47 51 eqtr2d 
 |-  ( ( ph /\ ( w e. _om /\ ( R ` w ) = <. v , z >. ) ) -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) )
53 52 rexlimdvaa 
 |-  ( ph -> ( E. w e. _om ( R ` w ) = <. v , z >. -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
54 34 53 sylbid 
 |-  ( ph -> ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
55 54 alrimiv 
 |-  ( ph -> A. z ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
56 fvex 
 |-  ( 2nd ` ( R ` ( `' G ` v ) ) ) e. _V
57 eqeq2 
 |-  ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( z = w <-> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) )
58 57 imbi2d 
 |-  ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( ( <. v , z >. e. S -> z = w ) <-> ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) ) )
59 58 albidv 
 |-  ( w = ( 2nd ` ( R ` ( `' G ` v ) ) ) -> ( A. z ( <. v , z >. e. S -> z = w ) <-> A. z ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) ) )
60 56 59 spcev 
 |-  ( A. z ( <. v , z >. e. S -> z = ( 2nd ` ( R ` ( `' G ` v ) ) ) ) -> E. w A. z ( <. v , z >. e. S -> z = w ) )
61 55 60 syl 
 |-  ( ph -> E. w A. z ( <. v , z >. e. S -> z = w ) )
62 61 alrimiv 
 |-  ( ph -> A. v E. w A. z ( <. v , z >. e. S -> z = w ) )
63 dffun5 
 |-  ( Fun S <-> ( Rel S /\ A. v E. w A. z ( <. v , z >. e. S -> z = w ) ) )
64 30 62 63 sylanbrc 
 |-  ( ph -> Fun S )
65 dmss 
 |-  ( S C_ ( Z X. _V ) -> dom S C_ dom ( Z X. _V ) )
66 27 65 syl 
 |-  ( ph -> dom S C_ dom ( Z X. _V ) )
67 dmxpss 
 |-  dom ( Z X. _V ) C_ Z
68 66 67 sstrdi 
 |-  ( ph -> dom S C_ Z )
69 1 2 3 4 5 noseqrdglem 
 |-  ( ( ph /\ v e. Z ) -> <. v , ( 2nd ` ( R ` ( `' G ` v ) ) ) >. e. ran R )
70 6 adantr 
 |-  ( ( ph /\ v e. Z ) -> S = ran R )
71 69 70 eleqtrrd 
 |-  ( ( ph /\ v e. Z ) -> <. v , ( 2nd ` ( R ` ( `' G ` v ) ) ) >. e. S )
72 48 56 opeldm 
 |-  ( <. v , ( 2nd ` ( R ` ( `' G ` v ) ) ) >. e. S -> v e. dom S )
73 71 72 syl 
 |-  ( ( ph /\ v e. Z ) -> v e. dom S )
74 68 73 eqelssd 
 |-  ( ph -> dom S = Z )
75 df-fn 
 |-  ( S Fn Z <-> ( Fun S /\ dom S = Z ) )
76 64 74 75 sylanbrc 
 |-  ( ph -> S Fn Z )