Metamath Proof Explorer

Theorem om2noseqrdg

Description: A helper lemma for the value of a recursive definition generator on a surreal sequence with characteristic function F ( x , y ) and initial value A . (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 om2noseqrdg 
|- ( ( ph /\ B e. _om ) -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` 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 fveq2 
 |-  ( z = (/) -> ( R ` z ) = ( R ` (/) ) )
7 fveq2 
 |-  ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
8 2fveq3 
 |-  ( z = (/) -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` (/) ) ) )
9 7 8 opeq12d 
 |-  ( z = (/) -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
10 6 9 eqeq12d 
 |-  ( z = (/) -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) )
11 10 imbi2d 
 |-  ( z = (/) -> ( ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) <-> ( ph -> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) ) )
12 fveq2 
 |-  ( z = v -> ( R ` z ) = ( R ` v ) )
13 fveq2 
 |-  ( z = v -> ( G ` z ) = ( G ` v ) )
14 2fveq3 
 |-  ( z = v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` v ) ) )
15 13 14 opeq12d 
 |-  ( z = v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
16 12 15 eqeq12d 
 |-  ( z = v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
17 16 imbi2d 
 |-  ( z = v -> ( ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) <-> ( ph -> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) )
18 fveq2 
 |-  ( z = suc v -> ( R ` z ) = ( R ` suc v ) )
19 fveq2 
 |-  ( z = suc v -> ( G ` z ) = ( G ` suc v ) )
20 2fveq3 
 |-  ( z = suc v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` suc v ) ) )
21 19 20 opeq12d 
 |-  ( z = suc v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
22 18 21 eqeq12d 
 |-  ( z = suc v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) )
23 22 imbi2d 
 |-  ( z = suc v -> ( ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) <-> ( ph -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) ) )
24 fveq2 
 |-  ( z = B -> ( R ` z ) = ( R ` B ) )
25 fveq2 
 |-  ( z = B -> ( G ` z ) = ( G ` B ) )
26 2fveq3 
 |-  ( z = B -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` B ) ) )
27 25 26 opeq12d 
 |-  ( z = B -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )
28 24 27 eqeq12d 
 |-  ( z = B -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) )
29 28 imbi2d 
 |-  ( z = B -> ( ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) <-> ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) ) )
30 5 fveq1d 
 |-  ( ph -> ( R ` (/) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) )
31 opex 
 |-  <. C , A >. e. _V
32 fr0g 
 |-  ( <. C , A >. e. _V -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >. )
33 31 32 ax-mp 
 |-  ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` (/) ) = <. C , A >.
34 30 33 eqtrdi 
 |-  ( ph -> ( R ` (/) ) = <. C , A >. )
35 1 2 om2noseq0 
 |-  ( ph -> ( G ` (/) ) = C )
36 34 fveq2d 
 |-  ( ph -> ( 2nd ` ( R ` (/) ) ) = ( 2nd ` <. C , A >. ) )
37 op2ndg 
 |-  ( ( C e. No /\ A e. V ) -> ( 2nd ` <. C , A >. ) = A )
38 1 4 37 syl2anc 
 |-  ( ph -> ( 2nd ` <. C , A >. ) = A )
39 36 38 eqtrd 
 |-  ( ph -> ( 2nd ` ( R ` (/) ) ) = A )
40 35 39 opeq12d 
 |-  ( ph -> <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. = <. C , A >. )
41 34 40 eqtr4d 
 |-  ( ph -> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
42 frsuc 
 |-  ( v e. _om -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc v ) = ( ( 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 ) ` v ) ) )
43 42 adantl 
 |-  ( ( ph /\ v e. _om ) -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc v ) = ( ( 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 ) ` v ) ) )
44 5 fveq1d 
 |-  ( ph -> ( R ` suc v ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc v ) )
45 44 adantr 
 |-  ( ( ph /\ v e. _om ) -> ( R ` suc v ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc v ) )
46 5 fveq1d 
 |-  ( ph -> ( R ` v ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` v ) )
47 46 fveq2d 
 |-  ( ph -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( 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 ) ` v ) ) )
48 47 adantr 
 |-  ( ( ph /\ v e. _om ) -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( 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 ) ` v ) ) )
49 43 45 48 3eqtr4d 
 |-  ( ( ph /\ v e. _om ) -> ( R ` suc v ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) )
50 49 adantrr 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( R ` suc v ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) )
51 fveq2 
 |-  ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
52 df-ov 
 |-  ( ( G ` v ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
53 fvex 
 |-  ( G ` v ) e. _V
54 fvex 
 |-  ( 2nd ` ( R ` v ) ) e. _V
55 oveq1 
 |-  ( w = ( G ` v ) -> ( w +s 1s ) = ( ( G ` v ) +s 1s ) )
56 oveq1 
 |-  ( w = ( G ` v ) -> ( w F z ) = ( ( G ` v ) F z ) )
57 55 56 opeq12d 
 |-  ( w = ( G ` v ) -> <. ( w +s 1s ) , ( w F z ) >. = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F z ) >. )
58 oveq2 
 |-  ( z = ( 2nd ` ( R ` v ) ) -> ( ( G ` v ) F z ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
59 58 opeq2d 
 |-  ( z = ( 2nd ` ( R ` v ) ) -> <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F z ) >. = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
60 oveq1 
 |-  ( x = w -> ( x +s 1s ) = ( w +s 1s ) )
61 oveq1 
 |-  ( x = w -> ( x F y ) = ( w F y ) )
62 60 61 opeq12d 
 |-  ( x = w -> <. ( x +s 1s ) , ( x F y ) >. = <. ( w +s 1s ) , ( w F y ) >. )
63 oveq2 
 |-  ( y = z -> ( w F y ) = ( w F z ) )
64 63 opeq2d 
 |-  ( y = z -> <. ( w +s 1s ) , ( w F y ) >. = <. ( w +s 1s ) , ( w F z ) >. )
65 62 64 cbvmpov 
 |-  ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) = ( w e. _V , z e. _V |-> <. ( w +s 1s ) , ( w F z ) >. )
66 opex 
 |-  <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. e. _V
67 57 59 65 66 ovmpo 
 |-  ( ( ( G ` v ) e. _V /\ ( 2nd ` ( R ` v ) ) e. _V ) -> ( ( G ` v ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
68 53 54 67 mp2an 
 |-  ( ( G ` v ) ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >.
69 52 68 eqtr3i 
 |-  ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >.
70 51 69 eqtrdi 
 |-  ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
71 70 ad2antll 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x F y ) >. ) ` ( R ` v ) ) = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
72 50 71 eqtrd 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( R ` suc v ) = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
73 1 adantr 
 |-  ( ( ph /\ v e. _om ) -> C e. No )
74 2 adantr 
 |-  ( ( ph /\ v e. _om ) -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
75 simpr 
 |-  ( ( ph /\ v e. _om ) -> v e. _om )
76 73 74 75 om2noseqsuc 
 |-  ( ( ph /\ v e. _om ) -> ( G ` suc v ) = ( ( G ` v ) +s 1s ) )
77 76 adantrr 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( G ` suc v ) = ( ( G ` v ) +s 1s ) )
78 72 fveq2d 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( 2nd ` ( R ` suc v ) ) = ( 2nd ` <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) )
79 ovex 
 |-  ( ( G ` v ) +s 1s ) e. _V
80 ovex 
 |-  ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. _V
81 79 80 op2nd 
 |-  ( 2nd ` <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) )
82 78 81 eqtrdi 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( 2nd ` ( R ` suc v ) ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
83 77 82 opeq12d 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. = <. ( ( G ` v ) +s 1s ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
84 72 83 eqtr4d 
 |-  ( ( ph /\ ( v e. _om /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) ) -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
85 84 exp32 
 |-  ( ph -> ( v e. _om -> ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) ) )
86 85 com12 
 |-  ( v e. _om -> ( ph -> ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) ) )
87 86 a2d 
 |-  ( v e. _om -> ( ( ph -> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( ph -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) ) )
88 11 17 23 29 41 87 finds 
 |-  ( B e. _om -> ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) )
89 88 impcom 
 |-  ( ( ph /\ B e. _om ) -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )