Theorem seqex 13126

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 13125	. 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
2		rdgfun 7797	. . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
3		omex 8839	. . 3 ⊢ ω ∈ V
4		funimaexg 6222	. . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V)
5	2, 3, 4	mp2an 682	. 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω) ∈ V
6	1, 5	eqeltri 2855	1 ⊢ seq𝑀( + , 𝐹) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3398  ⟨cop 4404   “ cima 5360  Fun wfun 6131  ‘cfv 6137  (class class class)co 6924   ↦ cmpt2 6926  ωcom 7345  reccrdg 7790  1c1 10275   + caddc 10277  seqcseq 13124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-om 7346  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-seq 13125

This theorem is referenced by:  seqshft  14238  clim2ser  14802  clim2ser2  14803  isermulc2  14805  isershft  14811  isercoll  14815  isercoll2  14816  iseralt  14832  fsumcvg  14859  sumrb  14860  isumclim3  14904  isumadd  14912  cvgcmp  14961  cvgcmpce  14963  trireciplem  15007  geolim  15014  geolim2  15015  geo2lim  15019  geomulcvg  15020  geoisum1c  15024  cvgrat  15027  mertens  15030  clim2prod  15032  clim2div  15033  ntrivcvg  15041  ntrivcvgfvn0  15043  ntrivcvgmullem  15045  fprodcvg  15072  prodrblem2  15073  fprodntriv  15084  iprodclim3  15142  iprodmul  15145  efcj  15233  eftlub  15250  eflegeo  15262  rpnnen2lem5  15360  mulgfval  17940  ovoliunnul  23722  ioombl1lem4  23776  vitalilem5  23827  dvnfval  24133  aaliou3lem3  24547  dvradcnv  24623  pserulm  24624  abelthlem6  24638  abelthlem7  24640  abelthlem9  24642  logtayllem  24853  logtayl  24854  atantayl  25126  leibpilem2  25131  leibpi  25132  log2tlbnd  25135  zetacvg  25204  lgamgulm2  25225  lgamcvglem  25229  lgamcvg2  25244  dchrisumlem3  25649  dchrisum0re  25671  esumcvgsum  30756  sseqval  31057  iprodgam  32230  faclim  32234  knoppcnlem6  33079  knoppcnlem9  33082  knoppndvlem4  33096  knoppndvlem6  33098  knoppf  33116  geomcau  34188  dvradcnv2  39516  binomcxplemnotnn0  39525  sumnnodd  40784  stirlinglem5  41236  stirlinglem7  41238  fourierdlem112  41376  sge0isum  41582