Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fmpt | Structured version Visualization version GIF 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 6496 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴) |
3 | 1 | rnmpt 5809 | . . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} |
4 | r19.29 3166 | . . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶)) | |
5 | eleq1 2818 | . . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵)) | |
6 | 5 | biimparc 483 | . . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
7 | 6 | rexlimivw 3191 | . . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
8 | 4, 7 | syl 17 | . . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
9 | 8 | ex 416 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵)) |
10 | 9 | abssdv 3968 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵) |
11 | 3, 10 | eqsstrid 3935 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵) |
12 | df-f 6362 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
13 | 2, 11, 12 | sylanbrc 586 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵) |
14 | fimacnv 6545 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) | |
15 | 1 | mptpreima 6081 | . . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} |
16 | 14, 15 | eqtr3di 2786 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}) |
17 | rabid2 3283 | . . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) | |
18 | 16, 17 | sylib 221 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) |
19 | 13, 18 | impbii 212 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2112 {cab 2714 ∀wral 3051 ∃wrex 3052 {crab 3055 ⊆ wss 3853 ↦ cmpt 5120 ◡ccnv 5535 ran crn 5537 “ cima 5539 Fn wfn 6353 ⟶wf 6354 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-br 5040 df-opab 5102 df-mpt 5121 df-id 5440 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-fun 6360 df-fn 6361 df-f 6362 |
This theorem is referenced by: f1ompt 6906 fmpti 6907 fvmptelrn 6908 fmptd 6909 fmptdf 6912 rnmptss 6917 f1oresrab 6920 idref 6939 f1mpt 7051 f1stres 7763 f2ndres 7764 fmpox 7815 fmpoco 7841 onoviun 8058 onnseq 8059 mptelixpg 8594 dom2lem 8646 iinfi 9011 cantnfrescl 9269 acni2 9625 acnlem 9627 dfac4 9701 dfacacn 9720 fin23lem28 9919 axdc2lem 10027 axcclem 10036 ac6num 10058 uzf 12406 ccatalpha 14115 repsf 14303 rlim2 15022 rlimi 15039 o1fsum 15340 ackbijnn 15355 pcmptcl 16407 vdwlem11 16507 ismon2 17193 isepi2 17200 yonedalem3b 17741 smndex1gbas 18283 efgsf 19073 gsummhm2 19278 gsummptcl 19306 gsummptfif1o 19307 gsummptfzcl 19308 gsumcom2 19314 gsummptnn0fz 19325 issrngd 19851 ipcl 20549 subrgasclcl 20979 evl1sca 21204 mavmulcl 21398 m2detleiblem3 21480 m2detleiblem4 21481 iinopn 21753 ordtrest2 22055 iscnp2 22090 discmp 22249 2ndcdisj 22307 ptunimpt 22446 pttopon 22447 ptcnplem 22472 upxp 22474 txdis1cn 22486 cnmpt11 22514 cnmpt21 22522 cnmptkp 22531 cnmptk1 22532 cnmpt1k 22533 cnmptkk 22534 cnmptk1p 22536 qtopeu 22567 uzrest 22748 txflf 22857 clsnsg 22961 tgpconncomp 22964 tsmsf1o 22996 prdsmet 23222 fsumcn 23721 cncfmpt1f 23765 iccpnfcnv 23795 lebnumlem1 23812 copco 23869 pcoass 23875 bcth3 24182 voliun 24405 i1f1lem 24540 iblcnlem 24640 limcvallem 24722 ellimc2 24728 cnmptlimc 24741 dvle 24858 dvfsumle 24872 dvfsumge 24873 dvfsumabs 24874 dvfsumlem2 24878 itgsubstlem 24899 sincn 25290 coscn 25291 rlimcxp 25810 harmonicbnd 25840 harmonicbnd2 25841 lgamgulmlem6 25870 sqff1o 26018 lgseisenlem3 26212 fmptdF 30667 ordtrest2NEW 31541 ddemeas 31870 eulerpartgbij 32005 0rrv 32084 reprpmtf1o 32272 subfacf 32804 tailf 34250 fdc 35589 heiborlem5 35659 3factsumint 39716 dvle2 39762 elrfirn2 40162 mptfcl 40186 mzpexpmpt 40211 mzpsubst 40214 rabdiophlem1 40267 rabdiophlem2 40268 pw2f1ocnv 40503 refsumcn 42187 fompt 42344 fmptf 42396 fprodcnlem 42758 dvsinax 43072 itgsubsticclem 43134 fargshiftf 44508 isomuspgrlem2b 44897 |
Copyright terms: Public domain | W3C validator |