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 7110

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 6691	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5955	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3115	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2822	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 481	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3152	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 414	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4066	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 4031	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6548	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 584	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6740	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6238	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2788	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3465	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 217	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 {cab 2710 ∀wral 3062 ∃wrex 3071 {crab 3433 ⊆ wss 3949 ↦ cmpt 5232 ^◡ccnv 5676 ran crn 5678 “ cima 5680 Fn wfn 6539 ⟶wf 6540

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-fun 6546 df-fn 6547 df-f 6548

This theorem is referenced by: f1ompt 7111 fmpti 7112 fvmptelcdm 7113 fmptd 7114 fmptdf 7117 rnmptss 7122 f1oresrab 7125 idref 7144 f1mpt 7260 f1stres 7999 f2ndres 8000 fmpox 8053 fmpoco 8081 onoviun 8343 onnseq 8344 mptelixpg 8929 dom2lem 8988 iinfi 9412 cantnfrescl 9671 acni2 10041 acnlem 10043 dfac4 10117 dfacacn 10136 fin23lem28 10335 axdc2lem 10443 axcclem 10452 ac6num 10474 uzf 12825 ccatalpha 14543 repsf 14723 rlim2 15440 rlimi 15457 o1fsum 15759 ackbijnn 15774 pcmptcl 16824 vdwlem11 16924 ismon2 17681 isepi2 17688 yonedalem3b 18232 smndex1gbas 18783 efgsf 19597 gsummhm2 19807 gsummptcl 19835 gsummptfif1o 19836 gsummptfzcl 19837 gsumcom2 19843 gsummptnn0fz 19854 issrngd 20469 ipcl 21186 subrgasclcl 21628 evl1sca 21853 mavmulcl 22049 m2detleiblem3 22131 m2detleiblem4 22132 iinopn 22404 ordtrest2 22708 iscnp2 22743 discmp 22902 2ndcdisj 22960 ptunimpt 23099 pttopon 23100 ptcnplem 23125 upxp 23127 txdis1cn 23139 cnmpt11 23167 cnmpt21 23175 cnmptkp 23184 cnmptk1 23185 cnmpt1k 23186 cnmptkk 23187 cnmptk1p 23189 qtopeu 23220 uzrest 23401 txflf 23510 clsnsg 23614 tgpconncomp 23617 tsmsf1o 23649 prdsmet 23876 fsumcn 24386 cncfmpt1f 24430 iccpnfcnv 24460 lebnumlem1 24477 copco 24534 pcoass 24540 bcth3 24848 voliun 25071 i1f1lem 25206 iblcnlem 25306 limcvallem 25388 ellimc2 25394 cnmptlimc 25407 dvle 25524 dvfsumle 25538 dvfsumge 25539 dvfsumabs 25540 dvfsumlem2 25544 itgsubstlem 25565 sincn 25956 coscn 25957 rlimcxp 26478 harmonicbnd 26508 harmonicbnd2 26509 lgamgulmlem6 26538 sqff1o 26686 lgseisenlem3 26880 fmptdF 31881 ordtrest2NEW 32903 ddemeas 33234 eulerpartgbij 33371 0rrv 33450 reprpmtf1o 33638 subfacf 34166 gg-dvfsumle 35182 gg-dvfsumlem2 35183 tailf 35260 fdc 36613 heiborlem5 36683 3factsumint 40890 dvle2 40937 fmpocos 41056 elrfirn2 41434 mptfcl 41458 mzpexpmpt 41483 mzpsubst 41486 rabdiophlem1 41539 rabdiophlem2 41540 pw2f1ocnv 41776 refsumcn 43714 fompt 43890 fmptf 43942 fmptff 43974 fprodcnlem 44315 dvsinax 44629 itgsubsticclem 44691 fargshiftf 46108 isomuspgrlem2b 46497

W3C validator