![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fmpt | Structured version Visualization version Unicode version |
Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
fmpt.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
fmpt |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fmpt.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | fnmpt 5686 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 1 | rnmpt 5058 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | r19.29 2893 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eleq1 2518 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | biimparc 494 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | rexlimivw 2850 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | syl 17 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | ex 440 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | abssdv 3471 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 3, 10 | syl5eqss 3444 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | df-f 5565 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 2, 11, 12 | sylanbrc 675 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 1 | mptpreima 5307 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | fimacnv 5996 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 14, 15 | syl5reqr 2501 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | rabid2 2936 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 16, 17 | sylib 201 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 13, 18 | impbii 192 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pr 4612 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3015 df-sbc 3236 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-br 4375 df-opab 4434 df-mpt 4435 df-id 4727 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-fv 5569 |
This theorem is referenced by: f1ompt 6028 fmpti 6029 fmptd 6030 fmptdf 6032 rnmptss 6037 f1oresrab 6040 idref 6132 f1mpt 6148 f1stres 6803 f2ndres 6804 fmpt2x 6847 fmpt2co 6867 onoviun 7049 onnseq 7050 mptelixpg 7546 dom2lem 7596 iinfi 7918 cantnfrescl 8168 acni2 8464 acnlem 8466 dfac4 8540 dfacacn 8558 fin23lem28 8757 axdc2lem 8865 axcclem 8874 ac6num 8896 uzf 11152 repsf 12875 rlim2 13571 rlimi 13588 rlimmptrcl 13682 lo1mptrcl 13696 o1mptrcl 13697 o1fsum 13884 ackbijnn 13897 pcmptcl 14847 vdwlem11 14952 ismon2 15650 isepi2 15657 yonedalem3b 16175 efgsf 17390 gsummhm2 17583 gsummptcl 17610 gsummptfif1o 17611 gsummptfzcl 17612 gsumcom2 17618 gsummptnn0fz 17626 issrngd 18100 psrass1lem 18612 subrgasclcl 18733 evl1sca 18933 ipcl 19211 frlmgsum 19341 uvcresum 19362 mavmulcl 19583 m2detleiblem3 19665 m2detleiblem4 19666 iinopn 19943 ordtrest2 20231 iscnp2 20266 discmp 20424 2ndcdisj 20482 ptunimpt 20621 pttopon 20622 txcnp 20646 ptcnplem 20647 ptcnp 20648 upxp 20649 ptcn 20653 txdis1cn 20661 cnmpt11 20689 cnmpt1t 20691 cnmpt12 20693 cnmpt21 20697 cnmptkp 20706 cnmptk1 20707 cnmpt1k 20708 cnmptkk 20709 cnmptk1p 20711 cnmptk2 20712 qtopeu 20742 uzrest 20923 txflf 21032 cnmpt1plusg 21113 clsnsg 21135 tgpconcomp 21138 tsmsf1o 21170 cnmpt1vsca 21219 prdsmet 21396 cnmpt1ds 21871 fsumcn 21913 cncfmpt1f 21956 cncfmpt2ss 21958 iccpnfcnv 21983 lebnumlem1 22000 lebnumlem1OLD 22003 copco 22060 pcoass 22066 cnmpt1ip 22229 bcth3 22310 voliun 22519 mbfmptcl 22605 i1f1lem 22659 i1fposd 22677 iblcnlem 22758 itgss3 22784 limcvallem 22838 ellimc2 22844 cnmptlimc 22857 dvmptcl 22925 dvmptco 22938 dvle 22971 dvfsumle 22985 dvfsumge 22986 dvfsumabs 22987 dvmptrecl 22988 dvfsumlem2 22991 itgparts 23011 itgsubstlem 23012 itgsubst 23013 ulmss 23364 ulmdvlem2 23368 itgulm2 23376 sincn 23411 coscn 23412 logtayl 23617 rlimcxp 23911 harmonicbnd 23941 harmonicbnd2 23942 lgamgulmlem6 23971 sqff1o 24121 lgseisenlem3 24291 fargshiftf 25376 fmptdF 28264 ordtrest2NEW 28736 ddemeas 29065 eulerpartgbij 29211 0rrv 29290 subfacf 29904 tailf 31037 fdc 32076 heiborlem5 32149 elrfirn2 35540 mptfcl 35564 mzpexpmpt 35589 mzpsubst 35592 rabdiophlem1 35646 rabdiophlem2 35647 pw2f1ocnv 35894 refsumcn 37348 mptex2 37443 fompt 37477 dvsinax 37825 itgsubsticclem 37894 |
Copyright terms: Public domain | W3C validator |