| 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 14008 | . 2 ⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) | |
| 2 | rdgfun 8380 | . . 3 ⊢ Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) | |
| 3 | omex 9591 | . . 3 ⊢ ω ∈ V | |
| 4 | funimaexg 6602 | . . 3 ⊢ ((Fun rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) ∧ ω ∈ V) → (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) ∈ V) | |
| 5 | 2, 3, 4 | mp2an 702 | . 2 ⊢ (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) ∈ V |
| 6 | 1, 5 | eqeltri 2857 | 1 ⊢ seq𝑀( + , 𝐹) ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2141 Vcvv 3453 〈cop 4585 “ cima 5646 Fun wfun 6509 ‘cfv 6515 (class class class)co 7390 ∈ cmpo 7392 ωcom 7840 reccrdg 8373 1c1 11067 + caddc 11069 seqcseq 14007 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pr 5387 ax-un 7712 ax-inf2 9589 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 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 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-ov 7393 df-om 7841 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-seq 14008 |
| This theorem is referenced by: seqshft 15091 clim2ser 15672 clim2ser2 15673 isermulc2 15675 isershft 15681 isercoll 15685 isercoll2 15686 iseralt 15702 fsumcvg 15729 sumrb 15730 isumclim3 15776 isumadd 15784 cvgcmp 15834 cvgcmpce 15836 trireciplem 15882 geolim 15890 geolim2 15891 geo2lim 15895 geomulcvg 15896 geoisum1c 15900 cvgrat 15903 mertens 15906 clim2prod 15908 clim2div 15909 ntrivcvg 15917 ntrivcvgfvn0 15919 ntrivcvgmullem 15921 fprodcvg 15950 prodrblem2 15951 fprodntriv 15962 iprodclim3 16020 iprodmul 16023 efcj 16112 eftlub 16131 eflegeo 16143 rpnnen2lem5 16240 mulgfvalALT 19102 ovoliunnul 25556 ioombl1lem4 25610 vitalilem5 25661 dvnfval 25971 aaliou3lem3 26395 dvradcnv 26471 pserulm 26472 abelthlem6 26486 abelthlem7 26488 abelthlem9 26490 logtayllem 26711 logtayl 26712 atantayl 26989 leibpilem2 26993 leibpi 26994 log2tlbnd 26997 zetacvg 27066 lgamgulm2 27087 lgamcvglem 27091 lgamcvg2 27106 dchrisumlem3 27542 dchrisum0re 27564 esumcvgsum 34345 sseqval 34645 iprodgam 36052 faclim 36056 knoppcnlem6 36896 knoppcnlem9 36899 knoppndvlem4 36913 knoppndvlem6 36915 knoppf 36933 geomcau 38218 dvradcnv2 44883 binomcxplemnotnn0 44892 sumnnodd 46166 stirlinglem5 46612 stirlinglem7 46614 fourierdlem112 46752 sge0isum 46961 itcoval 49243 |
| Copyright terms: Public domain | W3C validator |