Theorem seqeq2 11913

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

Assertion

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

Proof of Theorem seqeq2

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2452	. . . . 5 |- ( .+ = Q -> _V = _V )
2		oveq 6198	. . . . . 6 |- ( .+ = Q -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y Q ( F ` ( x + 1 ) ) ) )
3	2	opeq2d 4166	. . . . 5 |- ( .+ = Q -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( x + 1 ) , ( y Q ( F ` ( x + 1 ) ) ) >. )
4	1, 1, 3	mpt2eq123dv 6249	. . . 4 |- ( .+ = 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 ) ) ) >. ) )
5		rdgeq1 6969	. . . 4 |- ( ( 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 ) >. ) )
6	4, 5	syl 16	. . 3 |- ( .+ = 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 ) >. ) )
7	6	imaeq1d 5268	. 2 |- ( .+ = 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 ) )
8		df-seq 11910	. 2 |- seq M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " om )
9		df-seq 11910	. 2 |- seq M ( Q , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( y Q ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) " om )
10	7, 8, 9	3eqtr4g 2517	1 |- ( .+ = Q -> seq M ( .+ , F ) = seq M ( Q , F ) )

Syntax hints:   -> wi 4   = wceq 1370   _Vcvv 3070   <.cop 3983   "cima 4943   ` cfv 5518  (class class class)co 6192   |-> cmpt2 6194   omcom 6578   reccrdg 6967   1c1 9386   + caddc 9388   seqcseq 11909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-mpt 4452  df-cnv 4948  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5481  df-fv 5526  df-ov 6195  df-oprab 6196  df-mpt2 6197  df-recs 6934  df-rdg 6968  df-seq 11910

This theorem is referenced by:  seqeq2d  11916  sadcom  13763  gxfval  23881  ressmulgnn  26280  cvmliftlem15  27323