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 7085

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 6661	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5924	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3095	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2817	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3131	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4034	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3988	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6518	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6713	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6214	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2780	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3442	. . 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 2109 {cab 2708 ∀wral 3045 ∃wrex 3054 {crab 3408 ⊆ wss 3917 ↦ cmpt 5191 ^◡ccnv 5640 ran crn 5642 “ cima 5644 Fn wfn 6509 ⟶wf 6510

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pr 5390

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 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-sn 4593 df-pr 4595 df-op 4599 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-fun 6516 df-fn 6517 df-f 6518

This theorem is referenced by: f1ompt 7086 fmpti 7087 fvmptelcdm 7088 fmptd 7089 fmptdf 7092 fompt 7093 rnmptss 7098 f1oresrab 7102 idref 7121 f1mpt 7239 f1stres 7995 f2ndres 7996 fmpox 8049 fmpoco 8077 onoviun 8315 onnseq 8316 mptelixpg 8911 dom2lem 8966 iinfi 9375 cantnfrescl 9636 acni2 10006 acnlem 10008 dfac4 10082 dfacacn 10102 fin23lem28 10300 axdc2lem 10408 axcclem 10417 ac6num 10439 uzf 12803 ccatalpha 14565 repsf 14745 rlim2 15469 rlimi 15486 o1fsum 15786 ackbijnn 15801 pcmptcl 16869 vdwlem11 16969 ismon2 17703 isepi2 17710 yonedalem3b 18247 smndex1gbas 18836 efgsf 19666 gsummhm2 19876 gsummptcl 19904 gsummptfif1o 19905 gsummptfzcl 19906 gsumcom2 19912 gsummptnn0fz 19923 issrngd 20771 ipcl 21549 subrgasclcl 21981 evl1sca 22228 mavmulcl 22441 m2detleiblem3 22523 m2detleiblem4 22524 iinopn 22796 ordtrest2 23098 iscnp2 23133 discmp 23292 2ndcdisj 23350 ptunimpt 23489 pttopon 23490 ptcnplem 23515 upxp 23517 txdis1cn 23529 cnmpt11 23557 cnmpt21 23565 cnmptkp 23574 cnmptk1 23575 cnmpt1k 23576 cnmptkk 23577 cnmptk1p 23579 qtopeu 23610 uzrest 23791 txflf 23900 clsnsg 24004 tgpconncomp 24007 tsmsf1o 24039 prdsmet 24265 fsumcn 24768 cncfmpt1f 24814 iccpnfcnv 24849 lebnumlem1 24867 copco 24925 pcoass 24931 bcth3 25238 voliun 25462 i1f1lem 25597 iblcnlem 25697 limcvallem 25779 ellimc2 25785 cnmptlimc 25798 dvle 25919 dvfsumle 25933 dvfsumleOLD 25934 dvfsumge 25935 dvfsumabs 25936 dvfsumlem2 25940 dvfsumlem2OLD 25941 itgsubstlem 25962 sincn 26361 coscn 26362 rlimcxp 26891 harmonicbnd 26921 harmonicbnd2 26922 lgamgulmlem6 26951 sqff1o 27099 lgseisenlem3 27295 fmptdF 32587 ordtrest2NEW 33920 ddemeas 34233 eulerpartgbij 34370 0rrv 34449 reprpmtf1o 34624 subfacf 35169 tailf 36370 fdc 37746 heiborlem5 37816 3factsumint 42020 dvle2 42067 fmpocos 42229 elrfirn2 42691 mptfcl 42715 mzpexpmpt 42740 mzpsubst 42743 rabdiophlem1 42796 rabdiophlem2 42797 pw2f1ocnv 43033 refsumcn 45031 fmptf 45240 fmptff 45270 fprodcnlem 45604 dvsinax 45918 itgsubsticclem 45980 fargshiftf 47445

W3C validator