This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem seqeq2

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

Ref Expression
Assertion seqeq2 
|- ( .+ = Q -> seq M ( .+ , F ) = seq M ( Q , F ) )

Proof

Step Hyp Ref Expression
1 oveq 
 |-  ( .+ = Q -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y Q ( F ` ( x + 1 ) ) ) )
2 1 opeq2d 
 |-  ( .+ = Q -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( x + 1 ) , ( y Q ( F ` ( x + 1 ) ) ) >. )
3 2 mpoeq3dv 
 |-  ( .+ = Q -> ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y Q ( F ` ( x + 1 ) ) ) >. ) )
4 rdgeq1 
 |-  ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y Q ( F ` ( x + 1 ) ) ) >. ) -> 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 Q ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
5 3 4 syl 
 |-  ( .+ = Q -> 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 Q ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
6 5 imaeq1d 
 |-  ( .+ = Q -> ( 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 Q ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) )
7 df-seq 
 |-  seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
8 df-seq 
 |-  seq M ( Q , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y Q ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
9 6 7 8 3eqtr4g 
 |-  ( .+ = Q -> seq M ( .+ , F ) = seq M ( Q , F ) )