![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > seqex | Structured version Visualization version GIF version |
Description: Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.) |
Ref | Expression |
---|---|
seqex | ⊢ seq𝑀( + , 𝐹) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-seq 14000 | . 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) | |
2 | rdgfun 8437 | . . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) | |
3 | omex 9667 | . . 3 ⊢ ω ∈ V | |
4 | funimaexg 6639 | . . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) ∈ V) | |
5 | 2, 3, 4 | mp2an 691 | . 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) ∈ V |
6 | 1, 5 | eqeltri 2825 | 1 ⊢ seq𝑀( + , 𝐹) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3471 〈cop 4635 “ cima 5681 Fun wfun 6542 ‘cfv 6548 (class class class)co 7420 ∈ cmpo 7422 ωcom 7870 reccrdg 8430 1c1 11140 + caddc 11142 seqcseq 13999 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pr 5429 ax-un 7740 ax-inf2 9665 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-ral 3059 df-rex 3068 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-ov 7423 df-om 7871 df-2nd 7994 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-seq 14000 |
This theorem is referenced by: seqshft 15065 clim2ser 15634 clim2ser2 15635 isermulc2 15637 isershft 15643 isercoll 15647 isercoll2 15648 iseralt 15664 fsumcvg 15691 sumrb 15692 isumclim3 15738 isumadd 15746 cvgcmp 15795 cvgcmpce 15797 trireciplem 15841 geolim 15849 geolim2 15850 geo2lim 15854 geomulcvg 15855 geoisum1c 15859 cvgrat 15862 mertens 15865 clim2prod 15867 clim2div 15868 ntrivcvg 15876 ntrivcvgfvn0 15878 ntrivcvgmullem 15880 fprodcvg 15907 prodrblem2 15908 fprodntriv 15919 iprodclim3 15977 iprodmul 15980 efcj 16069 eftlub 16086 eflegeo 16098 rpnnen2lem5 16195 mulgfvalALT 19026 ovoliunnul 25449 ioombl1lem4 25503 vitalilem5 25554 dvnfval 25865 aaliou3lem3 26292 dvradcnv 26370 pserulm 26371 abelthlem6 26386 abelthlem7 26388 abelthlem9 26390 logtayllem 26606 logtayl 26607 atantayl 26882 leibpilem2 26886 leibpi 26887 log2tlbnd 26890 zetacvg 26960 lgamgulm2 26981 lgamcvglem 26985 lgamcvg2 27000 dchrisumlem3 27437 dchrisum0re 27459 esumcvgsum 33707 sseqval 34008 iprodgam 35336 faclim 35340 knoppcnlem6 35973 knoppcnlem9 35976 knoppndvlem4 35990 knoppndvlem6 35992 knoppf 36010 geomcau 37232 dvradcnv2 43784 binomcxplemnotnn0 43793 sumnnodd 45018 stirlinglem5 45466 stirlinglem7 45468 fourierdlem112 45606 sge0isum 45815 itcoval 47734 |
Copyright terms: Public domain | W3C validator |