# Metamath Proof Explorer

## Theorem seqeq3

Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

Ref Expression
Assertion seqeq3
`|- ( F = G -> seq M ( .+ , F ) = seq M ( .+ , G ) )`

### Proof

Step Hyp Ref Expression
1 fveq1
` |-  ( F = G -> ( F ` ( x + 1 ) ) = ( G ` ( x + 1 ) ) )`
2 1 oveq2d
` |-  ( F = G -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( G ` ( x + 1 ) ) ) )`
3 2 opeq2d
` |-  ( F = G -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. )`
4 3 mpoeq3dv
` |-  ( F = G -> ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) )`
5 fveq1
` |-  ( F = G -> ( F ` M ) = ( G ` M ) )`
6 5 opeq2d
` |-  ( F = G -> <. M , ( F ` M ) >. = <. M , ( G ` M ) >. )`
7 rdgeq12
` |-  ( ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) /\ <. M , ( F ` M ) >. = <. M , ( G ` M ) >. ) -> rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )`
8 4 6 7 syl2anc
` |-  ( F = G -> rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) )`
9 8 imaeq1d
` |-  ( F = G -> ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) " _om ) )`
10 df-seq
` |-  seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )`
11 df-seq
` |-  seq M ( .+ , G ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( G ` ( x + 1 ) ) ) >. ) , <. M , ( G ` M ) >. ) " _om )`
12 9 10 11 3eqtr4g
` |-  ( F = G -> seq M ( .+ , F ) = seq M ( .+ , G ) )`