Theorem seqex 13975

Description: Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)

Assertion

Ref	Expression
seqex	⊢ seq𝑀( + , 𝐹) ∈ V

Proof of Theorem seqex

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

Step	Hyp	Ref	Expression
1		df-seq 13974	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8387	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9603	. . 3 ⊢ ω ∈ V
4		funimaexg 6606	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 692	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2825	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ⟨cop 4598   “ cima 5644  Fun wfun 6508  ‘cfv 6514  (class class class)co 7390   ∈ cmpo 7392  ωcom 7845  reccrdg 8380  1c1 11076   + caddc 11078  seqcseq 13973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-inf2 9601

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-seq 13974

This theorem is referenced by:  seqshft  15058  clim2ser  15628  clim2ser2  15629  isermulc2  15631  isershft  15637  isercoll  15641  isercoll2  15642  iseralt  15658  fsumcvg  15685  sumrb  15686  isumclim3  15732  isumadd  15740  cvgcmp  15789  cvgcmpce  15791  trireciplem  15835  geolim  15843  geolim2  15844  geo2lim  15848  geomulcvg  15849  geoisum1c  15853  cvgrat  15856  mertens  15859  clim2prod  15861  clim2div  15862  ntrivcvg  15870  ntrivcvgfvn0  15872  ntrivcvgmullem  15874  fprodcvg  15903  prodrblem2  15904  fprodntriv  15915  iprodclim3  15973  iprodmul  15976  efcj  16065  eftlub  16084  eflegeo  16096  rpnnen2lem5  16193  mulgfvalALT  19009  ovoliunnul  25415  ioombl1lem4  25469  vitalilem5  25520  dvnfval  25831  aaliou3lem3  26259  dvradcnv  26337  pserulm  26338  abelthlem6  26353  abelthlem7  26355  abelthlem9  26357  logtayllem  26575  logtayl  26576  atantayl  26854  leibpilem2  26858  leibpi  26859  log2tlbnd  26862  zetacvg  26932  lgamgulm2  26953  lgamcvglem  26957  lgamcvg2  26972  dchrisumlem3  27409  dchrisum0re  27431  esumcvgsum  34085  sseqval  34386  iprodgam  35736  faclim  35740  knoppcnlem6  36493  knoppcnlem9  36496  knoppndvlem4  36510  knoppndvlem6  36512  knoppf  36530  geomcau  37760  dvradcnv2  44343  binomcxplemnotnn0  44352  sumnnodd  45635  stirlinglem5  46083  stirlinglem7  46085  fourierdlem112  46223  sge0isum  46432  itcoval  48654