fmpt - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fmpt		Structured version Visualization version GIF version

Theorem fmpt 7055

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)

**Hypothesis**
Ref	Expression
fmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)

**Assertion**
Ref	Expression
fmpt	⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 Allowed substitution hints: 𝐶(𝑥) 𝐹(𝑥)

Proof of Theorem fmpt Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
2	1	fnmpt 6632	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5906	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3099	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2824	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3133	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4019	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3972	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6684	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6196	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2786	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3432	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 218	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 {cab 2714 ∀wral 3051 ∃wrex 3060 {crab 3399 ⊆ wss 3901 ↦ cmpt 5179 ^◡ccnv 5623 ran crn 5625 “ cima 5627 Fn wfn 6487 ⟶wf 6488

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-fun 6494 df-fn 6495 df-f 6496

This theorem is referenced by: f1ompt 7056 fmpti 7057 fvmptelcdm 7058 fmptd 7059 fmptdf 7062 fompt 7063 rnmptss 7068 f1oresrab 7072 idref 7091 f1mpt 7207 f1stres 7957 f2ndres 7958 fmpox 8011 fmpoco 8037 onoviun 8275 onnseq 8276 mptelixpg 8873 dom2lem 8929 iinfi 9320 cantnfrescl 9585 acni2 9956 acnlem 9958 dfac4 10032 dfacacn 10052 fin23lem28 10250 axdc2lem 10358 axcclem 10367 ac6num 10389 uzf 12754 ccatalpha 14517 repsf 14696 rlim2 15419 rlimi 15436 o1fsum 15736 ackbijnn 15751 pcmptcl 16819 vdwlem11 16919 ismon2 17658 isepi2 17665 yonedalem3b 18202 smndex1gbas 18827 efgsf 19658 gsummhm2 19868 gsummptcl 19896 gsummptfif1o 19897 gsummptfzcl 19898 gsumcom2 19904 gsummptnn0fz 19915 issrngd 20788 ipcl 21588 subrgasclcl 22022 evl1sca 22278 mavmulcl 22491 m2detleiblem3 22573 m2detleiblem4 22574 iinopn 22846 ordtrest2 23148 iscnp2 23183 discmp 23342 2ndcdisj 23400 ptunimpt 23539 pttopon 23540 ptcnplem 23565 upxp 23567 txdis1cn 23579 cnmpt11 23607 cnmpt21 23615 cnmptkp 23624 cnmptk1 23625 cnmpt1k 23626 cnmptkk 23627 cnmptk1p 23629 qtopeu 23660 uzrest 23841 txflf 23950 clsnsg 24054 tgpconncomp 24057 tsmsf1o 24089 prdsmet 24314 fsumcn 24817 cncfmpt1f 24863 iccpnfcnv 24898 lebnumlem1 24916 copco 24974 pcoass 24980 bcth3 25287 voliun 25511 i1f1lem 25646 iblcnlem 25746 limcvallem 25828 ellimc2 25834 cnmptlimc 25847 dvle 25968 dvfsumle 25982 dvfsumleOLD 25983 dvfsumge 25984 dvfsumabs 25985 dvfsumlem2 25989 dvfsumlem2OLD 25990 itgsubstlem 26011 sincn 26410 coscn 26411 rlimcxp 26940 harmonicbnd 26970 harmonicbnd2 26971 lgamgulmlem6 27000 sqff1o 27148 lgseisenlem3 27344 mptelee 28967 fmptdF 32734 ordtrest2NEW 34080 ddemeas 34393 eulerpartgbij 34529 0rrv 34608 reprpmtf1o 34783 subfacf 35369 tailf 36569 fdc 37946 heiborlem5 38016 3factsumint 42279 dvle2 42326 fmpocos 42490 elrfirn2 42938 mptfcl 42962 mzpexpmpt 42987 mzpsubst 42990 rabdiophlem1 43043 rabdiophlem2 43044 pw2f1ocnv 43279 refsumcn 45275 fmptf 45483 fmptff 45513 fprodcnlem 45845 dvsinax 46157 itgsubsticclem 46219 fargshiftf 47686

W3C validator