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 6638 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴) |
3 | 1 | rnmpt 5908 | . . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} |
4 | r19.29 3115 | . . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶)) | |
5 | eleq1 2825 | . . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵)) | |
6 | 5 | biimparc 480 | . . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
7 | 6 | rexlimivw 3146 | . . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
8 | 4, 7 | syl 17 | . . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
9 | 8 | ex 413 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵)) |
10 | 9 | abssdv 4023 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵) |
11 | 3, 10 | eqsstrid 3990 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵) |
12 | df-f 6497 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
13 | 2, 11, 12 | sylanbrc 583 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵) |
14 | fimacnv 6687 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) | |
15 | 1 | mptpreima 6188 | . . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} |
16 | 14, 15 | eqtr3di 2791 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}) |
17 | rabid2 3434 | . . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) | |
18 | 16, 17 | sylib 217 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) |
19 | 13, 18 | impbii 208 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2713 ∀wral 3062 ∃wrex 3071 {crab 3405 ⊆ wss 3908 ↦ cmpt 5186 ◡ccnv 5630 ran crn 5632 “ cima 5634 Fn wfn 6488 ⟶wf 6489 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-fun 6495 df-fn 6496 df-f 6497 |
This theorem is referenced by: f1ompt 7055 fmpti 7056 fvmptelcdm 7057 fmptd 7058 fmptdf 7061 rnmptss 7066 f1oresrab 7069 idref 7088 f1mpt 7204 f1stres 7941 f2ndres 7942 fmpox 7995 fmpoco 8023 onoviun 8285 onnseq 8286 mptelixpg 8869 dom2lem 8928 iinfi 9349 cantnfrescl 9608 acni2 9978 acnlem 9980 dfac4 10054 dfacacn 10073 fin23lem28 10272 axdc2lem 10380 axcclem 10389 ac6num 10411 uzf 12762 ccatalpha 14473 repsf 14653 rlim2 15370 rlimi 15387 o1fsum 15690 ackbijnn 15705 pcmptcl 16755 vdwlem11 16855 ismon2 17609 isepi2 17616 yonedalem3b 18160 smndex1gbas 18704 efgsf 19502 gsummhm2 19707 gsummptcl 19735 gsummptfif1o 19736 gsummptfzcl 19737 gsumcom2 19743 gsummptnn0fz 19754 issrngd 20305 ipcl 21022 subrgasclcl 21459 evl1sca 21684 mavmulcl 21880 m2detleiblem3 21962 m2detleiblem4 21963 iinopn 22235 ordtrest2 22539 iscnp2 22574 discmp 22733 2ndcdisj 22791 ptunimpt 22930 pttopon 22931 ptcnplem 22956 upxp 22958 txdis1cn 22970 cnmpt11 22998 cnmpt21 23006 cnmptkp 23015 cnmptk1 23016 cnmpt1k 23017 cnmptkk 23018 cnmptk1p 23020 qtopeu 23051 uzrest 23232 txflf 23341 clsnsg 23445 tgpconncomp 23448 tsmsf1o 23480 prdsmet 23707 fsumcn 24217 cncfmpt1f 24261 iccpnfcnv 24291 lebnumlem1 24308 copco 24365 pcoass 24371 bcth3 24679 voliun 24902 i1f1lem 25037 iblcnlem 25137 limcvallem 25219 ellimc2 25225 cnmptlimc 25238 dvle 25355 dvfsumle 25369 dvfsumge 25370 dvfsumabs 25371 dvfsumlem2 25375 itgsubstlem 25396 sincn 25787 coscn 25788 rlimcxp 26307 harmonicbnd 26337 harmonicbnd2 26338 lgamgulmlem6 26367 sqff1o 26515 lgseisenlem3 26709 fmptdF 31458 ordtrest2NEW 32373 ddemeas 32704 eulerpartgbij 32841 0rrv 32920 reprpmtf1o 33108 subfacf 33638 tailf 34814 fdc 36171 heiborlem5 36241 3factsumint 40449 dvle2 40496 elrfirn2 40957 mptfcl 40981 mzpexpmpt 41006 mzpsubst 41009 rabdiophlem1 41062 rabdiophlem2 41063 pw2f1ocnv 41299 refsumcn 43177 fompt 43347 fmptf 43401 fmptff 43435 fprodcnlem 43772 dvsinax 44086 itgsubsticclem 44148 fargshiftf 45564 isomuspgrlem2b 45953 |
Copyright terms: Public domain | W3C validator |