Theorem seqex 14009

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 14008	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8380	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9591	. . 3 ⊢ ω ∈ V
4		funimaexg 6602	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 702	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2857	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ⟨cop 4585   “ cima 5646  Fun wfun 6509  ‘cfv 6515  (class class class)co 7390   ∈ cmpo 7392  ωcom 7840  reccrdg 8373  1c1 11067   + caddc 11069  seqcseq 14007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7712  ax-inf2 9589

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-om 7841  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-seq 14008

This theorem is referenced by:  seqshft  15091  clim2ser  15672  clim2ser2  15673  isermulc2  15675  isershft  15681  isercoll  15685  isercoll2  15686  iseralt  15702  fsumcvg  15729  sumrb  15730  isumclim3  15776  isumadd  15784  cvgcmp  15834  cvgcmpce  15836  trireciplem  15882  geolim  15890  geolim2  15891  geo2lim  15895  geomulcvg  15896  geoisum1c  15900  cvgrat  15903  mertens  15906  clim2prod  15908  clim2div  15909  ntrivcvg  15917  ntrivcvgfvn0  15919  ntrivcvgmullem  15921  fprodcvg  15950  prodrblem2  15951  fprodntriv  15962  iprodclim3  16020  iprodmul  16023  efcj  16112  eftlub  16131  eflegeo  16143  rpnnen2lem5  16240  mulgfvalALT  19102  ovoliunnul  25556  ioombl1lem4  25610  vitalilem5  25661  dvnfval  25971  aaliou3lem3  26395  dvradcnv  26471  pserulm  26472  abelthlem6  26486  abelthlem7  26488  abelthlem9  26490  logtayllem  26711  logtayl  26712  atantayl  26989  leibpilem2  26993  leibpi  26994  log2tlbnd  26997  zetacvg  27066  lgamgulm2  27087  lgamcvglem  27091  lgamcvg2  27106  dchrisumlem3  27542  dchrisum0re  27564  esumcvgsum  34345  sseqval  34645  iprodgam  36052  faclim  36056  knoppcnlem6  36896  knoppcnlem9  36899  knoppndvlem4  36913  knoppndvlem6  36915  knoppf  36933  geomcau  38218  dvradcnv2  44883  binomcxplemnotnn0  44892  sumnnodd  46166  stirlinglem5  46612  stirlinglem7  46614  fourierdlem112  46752  sge0isum  46961  itcoval  49243