Theorem seqex 13372

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 13371	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 8052	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 9106	. . 3 ⊢ ω ∈ V
4		funimaexg 6440	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 690	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2909	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494  ⟨cop 4573   “ cima 5558  Fun wfun 6349  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158  ωcom 7580  reccrdg 8045  1c1 10538   + caddc 10540  seqcseq 13370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-seq 13371

This theorem is referenced by:  seqshft  14444  clim2ser  15011  clim2ser2  15012  isermulc2  15014  isershft  15020  isercoll  15024  isercoll2  15025  iseralt  15041  fsumcvg  15069  sumrb  15070  isumclim3  15114  isumadd  15122  cvgcmp  15171  cvgcmpce  15173  trireciplem  15217  geolim  15226  geolim2  15227  geo2lim  15231  geomulcvg  15232  geoisum1c  15236  cvgrat  15239  mertens  15242  clim2prod  15244  clim2div  15245  ntrivcvg  15253  ntrivcvgfvn0  15255  ntrivcvgmullem  15257  fprodcvg  15284  prodrblem2  15285  fprodntriv  15296  iprodclim3  15354  iprodmul  15357  efcj  15445  eftlub  15462  eflegeo  15474  rpnnen2lem5  15571  mulgfvalALT  18227  ovoliunnul  24108  ioombl1lem4  24162  vitalilem5  24213  dvnfval  24519  aaliou3lem3  24933  dvradcnv  25009  pserulm  25010  abelthlem6  25024  abelthlem7  25026  abelthlem9  25028  logtayllem  25242  logtayl  25243  atantayl  25515  leibpilem2  25519  leibpi  25520  log2tlbnd  25523  zetacvg  25592  lgamgulm2  25613  lgamcvglem  25617  lgamcvg2  25632  dchrisumlem3  26067  dchrisum0re  26089  esumcvgsum  31347  sseqval  31646  iprodgam  32974  faclim  32978  knoppcnlem6  33837  knoppcnlem9  33840  knoppndvlem4  33854  knoppndvlem6  33856  knoppf  33874  geomcau  35049  dvradcnv2  40699  binomcxplemnotnn0  40708  sumnnodd  41931  stirlinglem5  42383  stirlinglem7  42385  fourierdlem112  42523  sge0isum  42729