Theorem seqex 13956

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 13955	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8348	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9555	. . 3 ⊢ ω ∈ V
4		funimaexg 6579	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 693	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2833	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ⟨cop 4574   “ cima 5627  Fun wfun 6486  ‘cfv 6492  (class class class)co 7360   ∈ cmpo 7362  ωcom 7810  reccrdg 8341  1c1 11030   + caddc 11032  seqcseq 13954

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-inf2 9553

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-seq 13955

This theorem is referenced by:  seqshft  15038  clim2ser  15608  clim2ser2  15609  isermulc2  15611  isershft  15617  isercoll  15621  isercoll2  15622  iseralt  15638  fsumcvg  15665  sumrb  15666  isumclim3  15712  isumadd  15720  cvgcmp  15770  cvgcmpce  15772  trireciplem  15818  geolim  15826  geolim2  15827  geo2lim  15831  geomulcvg  15832  geoisum1c  15836  cvgrat  15839  mertens  15842  clim2prod  15844  clim2div  15845  ntrivcvg  15853  ntrivcvgfvn0  15855  ntrivcvgmullem  15857  fprodcvg  15886  prodrblem2  15887  fprodntriv  15898  iprodclim3  15956  iprodmul  15959  efcj  16048  eftlub  16067  eflegeo  16079  rpnnen2lem5  16176  mulgfvalALT  19037  ovoliunnul  25484  ioombl1lem4  25538  vitalilem5  25589  dvnfval  25899  aaliou3lem3  26321  dvradcnv  26399  pserulm  26400  abelthlem6  26414  abelthlem7  26416  abelthlem9  26418  logtayllem  26636  logtayl  26637  atantayl  26914  leibpilem2  26918  leibpi  26919  log2tlbnd  26922  zetacvg  26992  lgamgulm2  27013  lgamcvglem  27017  lgamcvg2  27032  dchrisumlem3  27468  dchrisum0re  27490  esumcvgsum  34248  sseqval  34548  iprodgam  35940  faclim  35944  knoppcnlem6  36774  knoppcnlem9  36777  knoppndvlem4  36791  knoppndvlem6  36793  knoppf  36811  geomcau  38094  dvradcnv2  44792  binomcxplemnotnn0  44801  sumnnodd  46078  stirlinglem5  46524  stirlinglem7  46526  fourierdlem112  46664  sge0isum  46873  itcoval  49149