Theorem seqeq1 13968

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

Assertion

Ref	Expression
seqeq1	⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹))

Proof of Theorem seqeq1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6891	. . . . 5 ⊢ (𝑀 = 𝑁 → (𝐹‘𝑀) = (𝐹‘𝑁))
2		opeq12 4875	. . . . 5 ⊢ ((𝑀 = 𝑁 ∧ (𝐹‘𝑀) = (𝐹‘𝑁)) → ⟨𝑀, (𝐹‘𝑀)⟩ = ⟨𝑁, (𝐹‘𝑁)⟩)
3	1, 2	mpdan 685	. . . 4 ⊢ (𝑀 = 𝑁 → ⟨𝑀, (𝐹‘𝑀)⟩ = ⟨𝑁, (𝐹‘𝑁)⟩)
4		rdgeq2 8411	. . . 4 ⊢ (⟨𝑀, (𝐹‘𝑀)⟩ = ⟨𝑁, (𝐹‘𝑁)⟩ → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑁, (𝐹‘𝑁)⟩))
5	3, 4	syl 17	. . 3 ⊢ (𝑀 = 𝑁 → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑁, (𝐹‘𝑁)⟩))
6	5	imaeq1d 6058	. 2 ⊢ (𝑀 = 𝑁 → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑁, (𝐹‘𝑁)⟩) “ ω))
7		df-seq 13966	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
8		df-seq 13966	. 2 ⊢ seq𝑁( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑁, (𝐹‘𝑁)⟩) “ ω)
9	6, 7, 8	3eqtr4g 2797	1 ⊢ (𝑀 = 𝑁 → seq𝑀( + , 𝐹) = seq𝑁( + , 𝐹))

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3474  ⟨cop 4634   “ cima 5679  ‘cfv 6543  (class class class)co 7408   ∈ cmpo 7410  ωcom 7854  reccrdg 8408  1c1 11110   + caddc 11112  seqcseq 13965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5682  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fv 6551  df-ov 7411  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-seq 13966

This theorem is referenced by:  seqeq1d  13971  seqfn  13977  seq1  13978  seqp1  13980  seqf1olem2  14007  seqid  14012  seqz  14015  iserex  15602  summolem2  15661  summo  15662  zsum  15663  isumsplit  15785  ntrivcvg  15842  ntrivcvgn0  15843  ntrivcvgtail  15845  ntrivcvgmullem  15846  prodmolem2  15878  prodmo  15879  zprod  15880  fprodntriv  15885  ege2le3  16032  gsumval2a  18603  leibpi  26444  dvradcnv2  43096  binomcxplemnotnn0  43105  stirlinglem12  44791