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 7099

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 6677	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5937	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3101	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2822	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3137	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4043	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3997	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6534	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6727	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6227	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2785	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3449	. . 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 1540 ∈ wcel 2108 {cab 2713 ∀wral 3051 ∃wrex 3060 {crab 3415 ⊆ wss 3926 ↦ cmpt 5201 ^◡ccnv 5653 ran crn 5655 “ cima 5657 Fn wfn 6525 ⟶wf 6526

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ral 3052 df-rex 3061 df-rab 3416 df-v 3461 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-fun 6532 df-fn 6533 df-f 6534

This theorem is referenced by: f1ompt 7100 fmpti 7101 fvmptelcdm 7102 fmptd 7103 fmptdf 7106 fompt 7107 rnmptss 7112 f1oresrab 7116 idref 7135 f1mpt 7253 f1stres 8010 f2ndres 8011 fmpox 8064 fmpoco 8092 onoviun 8355 onnseq 8356 mptelixpg 8947 dom2lem 9004 iinfi 9427 cantnfrescl 9688 acni2 10058 acnlem 10060 dfac4 10134 dfacacn 10154 fin23lem28 10352 axdc2lem 10460 axcclem 10469 ac6num 10491 uzf 12853 ccatalpha 14609 repsf 14789 rlim2 15510 rlimi 15527 o1fsum 15827 ackbijnn 15842 pcmptcl 16909 vdwlem11 17009 ismon2 17745 isepi2 17752 yonedalem3b 18289 smndex1gbas 18878 efgsf 19708 gsummhm2 19918 gsummptcl 19946 gsummptfif1o 19947 gsummptfzcl 19948 gsumcom2 19954 gsummptnn0fz 19965 issrngd 20813 ipcl 21591 subrgasclcl 22023 evl1sca 22270 mavmulcl 22483 m2detleiblem3 22565 m2detleiblem4 22566 iinopn 22838 ordtrest2 23140 iscnp2 23175 discmp 23334 2ndcdisj 23392 ptunimpt 23531 pttopon 23532 ptcnplem 23557 upxp 23559 txdis1cn 23571 cnmpt11 23599 cnmpt21 23607 cnmptkp 23616 cnmptk1 23617 cnmpt1k 23618 cnmptkk 23619 cnmptk1p 23621 qtopeu 23652 uzrest 23833 txflf 23942 clsnsg 24046 tgpconncomp 24049 tsmsf1o 24081 prdsmet 24307 fsumcn 24810 cncfmpt1f 24856 iccpnfcnv 24891 lebnumlem1 24909 copco 24967 pcoass 24973 bcth3 25281 voliun 25505 i1f1lem 25640 iblcnlem 25740 limcvallem 25822 ellimc2 25828 cnmptlimc 25841 dvle 25962 dvfsumle 25976 dvfsumleOLD 25977 dvfsumge 25978 dvfsumabs 25979 dvfsumlem2 25983 dvfsumlem2OLD 25984 itgsubstlem 26005 sincn 26404 coscn 26405 rlimcxp 26934 harmonicbnd 26964 harmonicbnd2 26965 lgamgulmlem6 26994 sqff1o 27142 lgseisenlem3 27338 fmptdF 32580 ordtrest2NEW 33900 ddemeas 34213 eulerpartgbij 34350 0rrv 34429 reprpmtf1o 34604 subfacf 35143 tailf 36339 fdc 37715 heiborlem5 37785 3factsumint 41984 dvle2 42031 fmpocos 42232 elrfirn2 42666 mptfcl 42690 mzpexpmpt 42715 mzpsubst 42718 rabdiophlem1 42771 rabdiophlem2 42772 pw2f1ocnv 43008 refsumcn 45002 fmptf 45211 fmptff 45241 fprodcnlem 45576 dvsinax 45890 itgsubsticclem 45952 fargshiftf 47402

W3C validator