Theorem seqex 14071

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 14070	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8409	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9626	. . 3 ⊢ ω ∈ V
4		funimaexg 6623	. . 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 2858	1 ⊢ seq𝑀( + , 𝐹) ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  ⟨cop 4593   “ cima 5662  Fun wfun 6531  ‘cfv 6537  (class class class)co 7417   ∈ cmpo 7419  ωcom 7866  reccrdg 8402  1c1 11129   + caddc 11131  seqcseq 14069

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-inf2 9624

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  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 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seq 14070

This theorem is used by:  seqshft  15162  clim2ser  15746  clim2ser2  15747  isermulc2  15749  isershft  15755  isercoll  15759  isercoll2  15760  iseralt  15776  fsumcvg  15802  sumrb  15803  isumclim3  15849  isumadd  15857  cvgcmp  15907  cvgcmpce  15909  trireciplem  15955  geolim  15963  geolim2  15964  geo2lim  15968  geomulcvg  15969  geoisum1c  15973  cvgrat  15976  mertens  15979  clim2prod  15981  clim2div  15982  ntrivcvg  15990  ntrivcvgfvn0  15992  ntrivcvgmullem  15994  fprodcvg  16023  prodrblem2  16024  fprodntriv  16035  iprodclim3  16093  iprodmul  16096  efcj  16184  eftlub  16203  eflegeo  16215  rpnnen2lem5  16312  mulgfvalALT  19199  ovoliunnul  25741  ioombl1lem4  25795  vitalilem5  25846  dvnfval  26156  aaliou3lem3  26587  dvradcnv  26664  pserulm  26665  abelthlem6  26679  abelthlem7  26681  abelthlem9  26683  logtayllem  26904  logtayl  26905  atantayl  27182  leibpilem2  27186  leibpi  27187  log2tlbnd  27190  zetacvg  27259  lgamgulm2  27280  lgamcvglem  27284  lgamcvg2  27299  dchrisumlem3  27735  dchrisum0re  27757  esumcvgsum  34606  sseqval  34907  iprodgam  36329  faclim  36333  knoppcnlem6  37203  knoppcnlem9  37206  knoppndvlem4  37220  knoppndvlem6  37222  knoppf  37240  geomcau  38517  dvradcnv2  45179  binomcxplemnotnn0  45188  sumnnodd  46468  stirlinglem5  46914  stirlinglem7  46916  fourierdlem112  47054  sge0isum  47263  itcoval  49599