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 7038

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 6616	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5892	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3095	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2819	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3129	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4014	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3968	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6480	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6668	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6180	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2781	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3428	. . 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 2111 {cab 2709 ∀wral 3047 ∃wrex 3056 {crab 3395 ⊆ wss 3897 ↦ cmpt 5167 ^◡ccnv 5610 ran crn 5612 “ cima 5614 Fn wfn 6471 ⟶wf 6472

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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pr 5365

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 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4279 df-if 4471 df-sn 4572 df-pr 4574 df-op 4578 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5506 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-fun 6478 df-fn 6479 df-f 6480

This theorem is referenced by: f1ompt 7039 fmpti 7040 fvmptelcdm 7041 fmptd 7042 fmptdf 7045 fompt 7046 rnmptss 7051 f1oresrab 7055 idref 7074 f1mpt 7190 f1stres 7940 f2ndres 7941 fmpox 7994 fmpoco 8020 onoviun 8258 onnseq 8259 mptelixpg 8854 dom2lem 8909 iinfi 9296 cantnfrescl 9561 acni2 9932 acnlem 9934 dfac4 10008 dfacacn 10028 fin23lem28 10226 axdc2lem 10334 axcclem 10343 ac6num 10365 uzf 12730 ccatalpha 14496 repsf 14675 rlim2 15398 rlimi 15415 o1fsum 15715 ackbijnn 15730 pcmptcl 16798 vdwlem11 16898 ismon2 17636 isepi2 17643 yonedalem3b 18180 smndex1gbas 18805 efgsf 19636 gsummhm2 19846 gsummptcl 19874 gsummptfif1o 19875 gsummptfzcl 19876 gsumcom2 19882 gsummptnn0fz 19893 issrngd 20765 ipcl 21565 subrgasclcl 21997 evl1sca 22244 mavmulcl 22457 m2detleiblem3 22539 m2detleiblem4 22540 iinopn 22812 ordtrest2 23114 iscnp2 23149 discmp 23308 2ndcdisj 23366 ptunimpt 23505 pttopon 23506 ptcnplem 23531 upxp 23533 txdis1cn 23545 cnmpt11 23573 cnmpt21 23581 cnmptkp 23590 cnmptk1 23591 cnmpt1k 23592 cnmptkk 23593 cnmptk1p 23595 qtopeu 23626 uzrest 23807 txflf 23916 clsnsg 24020 tgpconncomp 24023 tsmsf1o 24055 prdsmet 24280 fsumcn 24783 cncfmpt1f 24829 iccpnfcnv 24864 lebnumlem1 24882 copco 24940 pcoass 24946 bcth3 25253 voliun 25477 i1f1lem 25612 iblcnlem 25712 limcvallem 25794 ellimc2 25800 cnmptlimc 25813 dvle 25934 dvfsumle 25948 dvfsumleOLD 25949 dvfsumge 25950 dvfsumabs 25951 dvfsumlem2 25955 dvfsumlem2OLD 25956 itgsubstlem 25977 sincn 26376 coscn 26377 rlimcxp 26906 harmonicbnd 26936 harmonicbnd2 26937 lgamgulmlem6 26966 sqff1o 27114 lgseisenlem3 27310 fmptdF 32630 ordtrest2NEW 33928 ddemeas 34241 eulerpartgbij 34377 0rrv 34456 reprpmtf1o 34631 subfacf 35211 tailf 36409 fdc 37785 heiborlem5 37855 3factsumint 42058 dvle2 42105 fmpocos 42267 elrfirn2 42729 mptfcl 42753 mzpexpmpt 42778 mzpsubst 42781 rabdiophlem1 42834 rabdiophlem2 42835 pw2f1ocnv 43070 refsumcn 45067 fmptf 45276 fmptff 45306 fprodcnlem 45639 dvsinax 45951 itgsubsticclem 46013 fargshiftf 47471

W3C validator