Theorem seqex 14176

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 14175	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8455	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9674	. . 3 ⊢ ω ∈ V
4		funimaexg 6651	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 705	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2860	1 ⊢ seq𝑀( + , 𝐹) ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ⟨cop 4838   “ cima 5659  Fun wfun 6555  ‘cfv 6561  (class class class)co 7446   ∈ cmpo 7448  ωcom 7904  reccrdg 8448  1c1 11231   + caddc 11233  seqcseq 14174

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778  ax-inf2 9672

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-seq 14175

This theorem is used by:  seqshft  15270  clim2ser  15854  clim2ser2  15855  isermulc2  15857  isershft  15863  isercoll  15867  isercoll2  15868  iseralt  15884  fsumcvg  15910  sumrb  15911  isumclim3  15957  isumadd  15965  cvgcmp  16015  cvgcmpce  16017  trireciplem  16063  geolim  16071  geolim2  16072  geo2lim  16076  geomulcvg  16077  geoisum1c  16081  cvgrat  16084  mertens  16087  clim2prod  16089  clim2div  16090  ntrivcvg  16098  ntrivcvgfvn0  16100  ntrivcvgmullem  16102  fprodcvg  16129  prodrblem2  16130  fprodntriv  16141  iprodclim3  16199  iprodmul  16202  efcj  16290  eftlub  16309  eflegeo  16321  rpnnen2lem5  16418  mulgfvalALT  19312  ovoliunnul  25861  ioombl1lem4  25915  vitalilem5  25966  dvnfval  26275  aaliou3lem3  26704  dvradcnv  26781  pserulm  26782  abelthlem6  26796  abelthlem7  26798  abelthlem9  26800  logtayllem  27020  logtayl  27021  atantayl  27298  leibpilem2  27302  leibpi  27303  log2tlbnd  27306  zetacvg  27375  lgamgulm2  27396  lgamcvglem  27400  lgamcvg2  27415  dchrisumlem3  27851  dchrisum0re  27873  esumcvgsum  34803  sseqval  35103  iprodgam  36698  faclim  36702  knoppcnlem6  37555  knoppcnlem9  37558  knoppndvlem4  37572  knoppndvlem6  37574  knoppf  37592  geomcau  38896  dvradcnv2  45534  binomcxplemnotnn0  45543  sumnnodd  46857  stirlinglem5  47303  stirlinglem7  47305  fourierdlem112  47443  sge0isum  47652  itcoval  49988