![]() |
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 6641 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴) |
3 | 1 | rnmpt 5910 | . . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} |
4 | r19.29 3117 | . . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶)) | |
5 | eleq1 2825 | . . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵)) | |
6 | 5 | biimparc 480 | . . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
7 | 6 | rexlimivw 3148 | . . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
8 | 4, 7 | syl 17 | . . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵) |
9 | 8 | ex 413 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵)) |
10 | 9 | abssdv 4025 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵) |
11 | 3, 10 | eqsstrid 3992 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵) |
12 | df-f 6500 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
13 | 2, 11, 12 | sylanbrc 583 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵) |
14 | fimacnv 6690 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) | |
15 | 1 | mptpreima 6190 | . . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} |
16 | 14, 15 | eqtr3di 2791 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}) |
17 | rabid2 3436 | . . 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 3064 ∃wrex 3073 {crab 3407 ⊆ wss 3910 ↦ cmpt 5188 ◡ccnv 5632 ran crn 5634 “ cima 5636 Fn wfn 6491 ⟶wf 6492 |
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 5256 ax-nul 5263 ax-pr 5384 |
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 2889 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-fun 6498 df-fn 6499 df-f 6500 |
This theorem is referenced by: f1ompt 7059 fmpti 7060 fvmptelcdm 7061 fmptd 7062 fmptdf 7065 rnmptss 7070 f1oresrab 7073 idref 7092 f1mpt 7208 f1stres 7945 f2ndres 7946 fmpox 7999 fmpoco 8027 onoviun 8289 onnseq 8290 mptelixpg 8873 dom2lem 8932 iinfi 9353 cantnfrescl 9612 acni2 9982 acnlem 9984 dfac4 10058 dfacacn 10077 fin23lem28 10276 axdc2lem 10384 axcclem 10393 ac6num 10415 uzf 12766 ccatalpha 14481 repsf 14661 rlim2 15378 rlimi 15395 o1fsum 15698 ackbijnn 15713 pcmptcl 16763 vdwlem11 16863 ismon2 17617 isepi2 17624 yonedalem3b 18168 smndex1gbas 18712 efgsf 19511 gsummhm2 19716 gsummptcl 19744 gsummptfif1o 19745 gsummptfzcl 19746 gsumcom2 19752 gsummptnn0fz 19763 issrngd 20320 ipcl 21037 subrgasclcl 21475 evl1sca 21700 mavmulcl 21896 m2detleiblem3 21978 m2detleiblem4 21979 iinopn 22251 ordtrest2 22555 iscnp2 22590 discmp 22749 2ndcdisj 22807 ptunimpt 22946 pttopon 22947 ptcnplem 22972 upxp 22974 txdis1cn 22986 cnmpt11 23014 cnmpt21 23022 cnmptkp 23031 cnmptk1 23032 cnmpt1k 23033 cnmptkk 23034 cnmptk1p 23036 qtopeu 23067 uzrest 23248 txflf 23357 clsnsg 23461 tgpconncomp 23464 tsmsf1o 23496 prdsmet 23723 fsumcn 24233 cncfmpt1f 24277 iccpnfcnv 24307 lebnumlem1 24324 copco 24381 pcoass 24387 bcth3 24695 voliun 24918 i1f1lem 25053 iblcnlem 25153 limcvallem 25235 ellimc2 25241 cnmptlimc 25254 dvle 25371 dvfsumle 25385 dvfsumge 25386 dvfsumabs 25387 dvfsumlem2 25391 itgsubstlem 25412 sincn 25803 coscn 25804 rlimcxp 26323 harmonicbnd 26353 harmonicbnd2 26354 lgamgulmlem6 26383 sqff1o 26531 lgseisenlem3 26725 fmptdF 31572 ordtrest2NEW 32504 ddemeas 32835 eulerpartgbij 32972 0rrv 33051 reprpmtf1o 33239 subfacf 33769 tailf 34847 fdc 36204 heiborlem5 36274 3factsumint 40482 dvle2 40529 elrfirn2 41005 mptfcl 41029 mzpexpmpt 41054 mzpsubst 41057 rabdiophlem1 41110 rabdiophlem2 41111 pw2f1ocnv 41347 refsumcn 43225 fompt 43401 fmptf 43455 fmptff 43488 fprodcnlem 43830 dvsinax 44144 itgsubsticclem 44206 fargshiftf 45622 isomuspgrlem2b 46011 |
Copyright terms: Public domain | W3C validator |