Theorem seqex 13963

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  ⟨cop 4568   “ cima 5628  Fun wfun 6486  ‘cfv 6492  (class class class)co 7363   ∈ cmpo 7365  ωcom 7813  reccrdg 8345  1c1 11037   + caddc 11039  seqcseq 13961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-inf2 9560

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-seq 13962

This theorem is referenced by:  seqshft  15045  clim2ser  15615  clim2ser2  15616  isermulc2  15618  isershft  15624  isercoll  15628  isercoll2  15629  iseralt  15645  fsumcvg  15672  sumrb  15673  isumclim3  15719  isumadd  15727  cvgcmp  15777  cvgcmpce  15779  trireciplem  15825  geolim  15833  geolim2  15834  geo2lim  15838  geomulcvg  15839  geoisum1c  15843  cvgrat  15846  mertens  15849  clim2prod  15851  clim2div  15852  ntrivcvg  15860  ntrivcvgfvn0  15862  ntrivcvgmullem  15864  fprodcvg  15893  prodrblem2  15894  fprodntriv  15905  iprodclim3  15963  iprodmul  15966  efcj  16055  eftlub  16074  eflegeo  16086  rpnnen2lem5  16183  mulgfvalALT  19044  ovoliunnul  25499  ioombl1lem4  25553  vitalilem5  25604  dvnfval  25914  aaliou3lem3  26335  dvradcnv  26411  pserulm  26412  abelthlem6  26426  abelthlem7  26428  abelthlem9  26430  logtayllem  26648  logtayl  26649  atantayl  26926  leibpilem2  26930  leibpi  26931  log2tlbnd  26934  zetacvg  27003  lgamgulm2  27024  lgamcvglem  27028  lgamcvg2  27043  dchrisumlem3  27479  dchrisum0re  27501  esumcvgsum  34279  sseqval  34579  iprodgam  35977  faclim  35981  knoppcnlem6  36811  knoppcnlem9  36814  knoppndvlem4  36828  knoppndvlem6  36830  knoppf  36848  geomcau  38133  dvradcnv2  44798  binomcxplemnotnn0  44807  sumnnodd  46082  stirlinglem5  46528  stirlinglem7  46530  fourierdlem112  46668  sge0isum  46877  itcoval  49159