Theorem seqex 14039

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 14038	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8403	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9612	. . 3 ⊢ ω ∈ V
4		funimaexg 6623	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 704	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2865	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ⟨cop 4600   “ cima 5665  Fun wfun 6531  ‘cfv 6537  (class class class)co 7411   ∈ cmpo 7413  ωcom 7862  reccrdg 8396  1c1 11101   + caddc 11103  seqcseq 14037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-inf2 9610

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-seq 14038

This theorem is referenced by:  seqshft  15122  clim2ser  15706  clim2ser2  15707  isermulc2  15709  isershft  15715  isercoll  15719  isercoll2  15720  iseralt  15736  fsumcvg  15763  sumrb  15764  isumclim3  15810  isumadd  15818  cvgcmp  15868  cvgcmpce  15870  trireciplem  15916  geolim  15924  geolim2  15925  geo2lim  15929  geomulcvg  15930  geoisum1c  15934  cvgrat  15937  mertens  15940  clim2prod  15942  clim2div  15943  ntrivcvg  15951  ntrivcvgfvn0  15953  ntrivcvgmullem  15955  fprodcvg  15984  prodrblem2  15985  fprodntriv  15996  iprodclim3  16054  iprodmul  16057  efcj  16146  eftlub  16165  eflegeo  16177  rpnnen2lem5  16274  mulgfvalALT  19136  ovoliunnul  25635  ioombl1lem4  25689  vitalilem5  25740  dvnfval  26050  aaliou3lem3  26474  dvradcnv  26550  pserulm  26551  abelthlem6  26565  abelthlem7  26567  abelthlem9  26569  logtayllem  26790  logtayl  26791  atantayl  27068  leibpilem2  27072  leibpi  27073  log2tlbnd  27076  zetacvg  27145  lgamgulm2  27166  lgamcvglem  27170  lgamcvg2  27185  dchrisumlem3  27621  dchrisum0re  27643  esumcvgsum  34423  sseqval  34723  iprodgam  36133  faclim  36137  knoppcnlem6  36976  knoppcnlem9  36979  knoppndvlem4  36993  knoppndvlem6  36995  knoppf  37013  geomcau  38298  dvradcnv2  44949  binomcxplemnotnn0  44958  sumnnodd  46238  stirlinglem5  46684  stirlinglem7  46686  fourierdlem112  46824  sge0isum  47033  itcoval  49326