Metamath Proof Explorer

Theorem seqseq123d

Description: Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses seqseq123d.1 
|- ( ph -> M = N )
seqseq123d.2 
|- ( ph -> .+ = Q )
seqseq123d.3 
|- ( ph -> F = G )
Assertion seqseq123d 
|- ( ph -> seq_s M ( .+ , F ) = seq_s N ( Q , G ) )

Proof

Step Hyp Ref Expression
1 seqseq123d.1 
 |-  ( ph -> M = N )
2 seqseq123d.2 
 |-  ( ph -> .+ = Q )
3 seqseq123d.3 
 |-  ( ph -> F = G )
4 2 oveqd 
 |-  ( ph -> ( y .+ ( F ` ( x +s 1s ) ) ) = ( y Q ( F ` ( x +s 1s ) ) ) )
5 3 fveq1d 
 |-  ( ph -> ( F ` ( x +s 1s ) ) = ( G ` ( x +s 1s ) ) )
6 5 oveq2d 
 |-  ( ph -> ( y Q ( F ` ( x +s 1s ) ) ) = ( y Q ( G ` ( x +s 1s ) ) ) )
7 4 6 eqtrd 
 |-  ( ph -> ( y .+ ( F ` ( x +s 1s ) ) ) = ( y Q ( G ` ( x +s 1s ) ) ) )
8 7 opeq2d 
 |-  ( ph -> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. = <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. )
9 8 mpoeq3dv 
 |-  ( ph -> ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. ) )
10 3 1 fveq12d 
 |-  ( ph -> ( F ` M ) = ( G ` N ) )
11 1 10 opeq12d 
 |-  ( ph -> <. M , ( F ` M ) >. = <. N , ( G ` N ) >. )
12 rdgeq12 
 |-  ( ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. ) /\ <. M , ( F ` M ) >. = <. N , ( G ` N ) >. ) -> rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. ) , <. N , ( G ` N ) >. ) )
13 9 11 12 syl2anc 
 |-  ( ph -> rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. ) , <. N , ( G ` N ) >. ) )
14 13 imaeq1d 
 |-  ( ph -> ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. ) , <. N , ( G ` N ) >. ) " _om ) )
15 df-seqs 
 |-  seq_s M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
16 df-seqs 
 |-  seq_s N ( Q , G ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y Q ( G ` ( x +s 1s ) ) ) >. ) , <. N , ( G ` N ) >. ) " _om )
17 14 15 16 3eqtr4g 
 |-  ( ph -> seq_s M ( .+ , F ) = seq_s N ( Q , G ) )