Theorem seqex 14026

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 14025	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8438	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9665	. . 3 ⊢ ω ∈ V
4		funimaexg 6633	. . 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 2829	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3463  ⟨cop 4612   “ cima 5668  Fun wfun 6535  ‘cfv 6541  (class class class)co 7413   ∈ cmpo 7415  ωcom 7869  reccrdg 8431  1c1 11138   + caddc 11140  seqcseq 14024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-inf2 9663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-seq 14025

This theorem is referenced by:  seqshft  15106  clim2ser  15673  clim2ser2  15674  isermulc2  15676  isershft  15682  isercoll  15686  isercoll2  15687  iseralt  15703  fsumcvg  15730  sumrb  15731  isumclim3  15777  isumadd  15785  cvgcmp  15834  cvgcmpce  15836  trireciplem  15880  geolim  15888  geolim2  15889  geo2lim  15893  geomulcvg  15894  geoisum1c  15898  cvgrat  15901  mertens  15904  clim2prod  15906  clim2div  15907  ntrivcvg  15915  ntrivcvgfvn0  15917  ntrivcvgmullem  15919  fprodcvg  15948  prodrblem2  15949  fprodntriv  15960  iprodclim3  16018  iprodmul  16021  efcj  16110  eftlub  16127  eflegeo  16139  rpnnen2lem5  16236  mulgfvalALT  19057  ovoliunnul  25478  ioombl1lem4  25532  vitalilem5  25583  dvnfval  25894  aaliou3lem3  26322  dvradcnv  26400  pserulm  26401  abelthlem6  26416  abelthlem7  26418  abelthlem9  26420  logtayllem  26637  logtayl  26638  atantayl  26916  leibpilem2  26920  leibpi  26921  log2tlbnd  26924  zetacvg  26994  lgamgulm2  27015  lgamcvglem  27019  lgamcvg2  27034  dchrisumlem3  27471  dchrisum0re  27493  esumcvgsum  34048  sseqval  34349  iprodgam  35701  faclim  35705  knoppcnlem6  36458  knoppcnlem9  36461  knoppndvlem4  36475  knoppndvlem6  36477  knoppf  36495  geomcau  37725  dvradcnv2  44323  binomcxplemnotnn0  44332  sumnnodd  45602  stirlinglem5  46050  stirlinglem7  46052  fourierdlem112  46190  sge0isum  46399  itcoval  48540