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 ) )