Theorem noseqrdgsuc

Description: Successor value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 19-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	noseqrdgsuc	|- ( ( ph /\ B e. Z ) -> ( S ` ( B +s 1s ) ) = ( B F ( S ` B ) ) )

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	adantr	|- ( ( ph /\ B e. Z ) -> S Fn Z )
9	8	fnfund	|- ( ( ph /\ B e. Z ) -> Fun S )
10	3	adantr	|- ( ( ph /\ B e. Z ) -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
11	1	adantr	|- ( ( ph /\ B e. Z ) -> C e. No )
12		simpr	|- ( ( ph /\ B e. Z ) -> B e. Z )
13	10 11 12	noseqp1	|- ( ( ph /\ B e. Z ) -> ( B +s 1s ) e. Z )
14	1 2 3 4 5	noseqrdglem	|- ( ( ph /\ ( B +s 1s ) e. Z ) -> <. ( B +s 1s ) , ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) >. e. ran R )
15	13 14	syldan	|- ( ( ph /\ B e. Z ) -> <. ( B +s 1s ) , ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) >. e. ran R )
16	6	adantr	|- ( ( ph /\ B e. Z ) -> S = ran R )
17	15 16	eleqtrrd	|- ( ( ph /\ B e. Z ) -> <. ( B +s 1s ) , ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) >. e. S )
18		funopfv	|- ( Fun S -> ( <. ( B +s 1s ) , ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) >. e. S -> ( S ` ( B +s 1s ) ) = ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) ) )
19	9 17 18	sylc	|- ( ( ph /\ B e. Z ) -> ( S ` ( B +s 1s ) ) = ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) )
20	1 2 3	om2noseqf1o	|- ( ph -> G : _om -1-1-onto-> Z )
21	20	adantr	|- ( ( ph /\ B e. Z ) -> G : _om -1-1-onto-> Z )
22		f1ocnvdm	|- ( ( G : _om -1-1-onto-> Z /\ B e. Z ) -> ( `' G ` B ) e. _om )
23	20 22	sylan	|- ( ( ph /\ B e. Z ) -> ( `' G ` B ) e. _om )
24		peano2	|- ( ( `' G ` B ) e. _om -> suc ( `' G ` B ) e. _om )
25	23 24	syl	|- ( ( ph /\ B e. Z ) -> suc ( `' G ` B ) e. _om )
26	21 25	jca	|- ( ( ph /\ B e. Z ) -> ( G : _om -1-1-onto-> Z /\ suc ( `' G ` B ) e. _om ) )
27	2	adantr	|- ( ( ph /\ B e. Z ) -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
28	11 27 23	om2noseqsuc	|- ( ( ph /\ B e. Z ) -> ( G ` suc ( `' G ` B ) ) = ( ( G ` ( `' G ` B ) ) +s 1s ) )
29		f1ocnvfv2	|- ( ( G : _om -1-1-onto-> Z /\ B e. Z ) -> ( G ` ( `' G ` B ) ) = B )
30	20 29	sylan	|- ( ( ph /\ B e. Z ) -> ( G ` ( `' G ` B ) ) = B )
31	30	oveq1d	|- ( ( ph /\ B e. Z ) -> ( ( G ` ( `' G ` B ) ) +s 1s ) = ( B +s 1s ) )
32	28 31	eqtrd	|- ( ( ph /\ B e. Z ) -> ( G ` suc ( `' G ` B ) ) = ( B +s 1s ) )
33		f1ocnvfv	|- ( ( G : _om -1-1-onto-> Z /\ suc ( `' G ` B ) e. _om ) -> ( ( G ` suc ( `' G ` B ) ) = ( B +s 1s ) -> ( `' G ` ( B +s 1s ) ) = suc ( `' G ` B ) ) )
34	26 32 33	sylc	|- ( ( ph /\ B e. Z ) -> ( `' G ` ( B +s 1s ) ) = suc ( `' G ` B ) )
35	34	fveq2d	|- ( ( ph /\ B e. Z ) -> ( R ` ( `' G ` ( B +s 1s ) ) ) = ( R ` suc ( `' G ` B ) ) )
36	35	fveq2d	|- ( ( ph /\ B e. Z ) -> ( 2nd ` ( R ` ( `' G ` ( B +s 1s ) ) ) ) = ( 2nd ` ( R ` suc ( `' G ` B ) ) ) )
37	19 36	eqtrd	|- ( ( ph /\ B e. Z ) -> ( S ` ( B +s 1s ) ) = ( 2nd ` ( R ` suc ( `' G ` B ) ) ) )
38		frsuc	|- ( ( `' G ` B ) e. _om -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc ( `' G ` B ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) ) )
39	38	adantl	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc ( `' G ` B ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) ) )
40	5	fveq1d	|- ( ph -> ( R ` suc ( `' G ` B ) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc ( `' G ` B ) ) )
41	40	adantr	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( R ` suc ( `' G ` B ) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc ( `' G ` B ) ) )
42	5	fveq1d	|- ( ph -> ( R ` ( `' G ` B ) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) )
43	42	fveq2d	|- ( ph -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) ) )
44	43	adantr	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) ) )
45	39 41 44	3eqtr4d	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( R ` suc ( `' G ` B ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) )
46	1 2 3 4 5	om2noseqrdg	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( R ` ( `' G ` B ) ) = <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
47	46	fveq2d	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. ) )
48		df-ov	|- ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
49	47 48	eqtr4di	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
50	45 49	eqtrd	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( R ` suc ( `' G ` B ) ) = ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
51		fvex	|- ( G ` ( `' G ` B ) ) e. _V
52		fvex	|- ( 2nd ` ( R ` ( `' G ` B ) ) ) e. _V
53		oveq1	|- ( z = ( G ` ( `' G ` B ) ) -> ( z +s 1s ) = ( ( G ` ( `' G ` B ) ) +s 1s ) )
54		oveq1	|- ( z = ( G ` ( `' G ` B ) ) -> ( z F w ) = ( ( G ` ( `' G ` B ) ) F w ) )
55	53 54	opeq12d	|- ( z = ( G ` ( `' G ` B ) ) -> <. ( z +s 1s ) , ( z F w ) >. = <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F w ) >. )
56		oveq2	|- ( w = ( 2nd ` ( R ` ( `' G ` B ) ) ) -> ( ( G ` ( `' G ` B ) ) F w ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
57	56	opeq2d	|- ( w = ( 2nd ` ( R ` ( `' G ` B ) ) ) -> <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F w ) >. = <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. )
58		oveq1	|- ( x = z -> ( x +s 1s ) = ( z +s 1s ) )
59		oveq1	|- ( x = z -> ( x F y ) = ( z F y ) )
60	58 59	opeq12d	|- ( x = z -> <. ( x +s 1s ) , ( x F y ) >. = <. ( z +s 1s ) , ( z F y ) >. )
61		oveq2	|- ( y = w -> ( z F y ) = ( z F w ) )
62	61	opeq2d	|- ( y = w -> <. ( z +s 1s ) , ( z F y ) >. = <. ( z +s 1s ) , ( z F w ) >. )
63	60 62	cbvmpov	|- ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) = ( z e. _V , w e. _V |-> <. ( z +s 1s ) , ( z F w ) >. )
64		opex	|- <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. e. _V
65	55 57 63 64	ovmpo	|- ( ( ( G ` ( `' G ` B ) ) e. _V /\ ( 2nd ` ( R ` ( `' G ` B ) ) ) e. _V ) -> ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. )
66	51 52 65	mp2an	|- ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >.
67	50 66	eqtrdi	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( R ` suc ( `' G ` B ) ) = <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. )
68	67	fveq2d	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( 2nd ` ( R ` suc ( `' G ` B ) ) ) = ( 2nd ` <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. ) )
69		ovex	|- ( ( G ` ( `' G ` B ) ) +s 1s ) e. _V
70		ovex	|- ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) e. _V
71	69 70	op2nd	|- ( 2nd ` <. ( ( G ` ( `' G ` B ) ) +s 1s ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) )
72	68 71	eqtrdi	|- ( ( ph /\ ( `' G ` B ) e. _om ) -> ( 2nd ` ( R ` suc ( `' G ` B ) ) ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
73	23 72	syldan	|- ( ( ph /\ B e. Z ) -> ( 2nd ` ( R ` suc ( `' G ` B ) ) ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
74	1 2 3 4 5	noseqrdglem	|- ( ( ph /\ B e. Z ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. ran R )
75	74 16	eleqtrrd	|- ( ( ph /\ B e. Z ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. S )
76		funopfv	|- ( Fun S -> ( <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. S -> ( S ` B ) = ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
77	9 75 76	sylc	|- ( ( ph /\ B e. Z ) -> ( S ` B ) = ( 2nd ` ( R ` ( `' G ` B ) ) ) )
78	77	eqcomd	|- ( ( ph /\ B e. Z ) -> ( 2nd ` ( R ` ( `' G ` B ) ) ) = ( S ` B ) )
79	30 78	oveq12d	|- ( ( ph /\ B e. Z ) -> ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = ( B F ( S ` B ) ) )
80	37 73 79	3eqtrd	|- ( ( ph /\ B e. Z ) -> ( S ` ( B +s 1s ) ) = ( B F ( S ` B ) ) )