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 7048

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 6626	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5903	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3092	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2816	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3126	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4022	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3976	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6490	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6678	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6191	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2779	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3430	. . 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 2707 ∀wral 3044 ∃wrex 3053 {crab 3396 ⊆ wss 3905 ↦ cmpt 5176 ^◡ccnv 5622 ran crn 5624 “ cima 5626 Fn wfn 6481 ⟶wf 6482

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 2701 ax-sep 5238 ax-nul 5248 ax-pr 5374

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ral 3045 df-rex 3054 df-rab 3397 df-v 3440 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-fun 6488 df-fn 6489 df-f 6490

This theorem is referenced by: f1ompt 7049 fmpti 7050 fvmptelcdm 7051 fmptd 7052 fmptdf 7055 fompt 7056 rnmptss 7061 f1oresrab 7065 idref 7084 f1mpt 7202 f1stres 7955 f2ndres 7956 fmpox 8009 fmpoco 8035 onoviun 8273 onnseq 8274 mptelixpg 8869 dom2lem 8924 iinfi 9326 cantnfrescl 9591 acni2 9959 acnlem 9961 dfac4 10035 dfacacn 10055 fin23lem28 10253 axdc2lem 10361 axcclem 10370 ac6num 10392 uzf 12757 ccatalpha 14519 repsf 14698 rlim2 15422 rlimi 15439 o1fsum 15739 ackbijnn 15754 pcmptcl 16822 vdwlem11 16922 ismon2 17660 isepi2 17667 yonedalem3b 18204 smndex1gbas 18795 efgsf 19627 gsummhm2 19837 gsummptcl 19865 gsummptfif1o 19866 gsummptfzcl 19867 gsumcom2 19873 gsummptnn0fz 19884 issrngd 20759 ipcl 21559 subrgasclcl 21991 evl1sca 22238 mavmulcl 22451 m2detleiblem3 22533 m2detleiblem4 22534 iinopn 22806 ordtrest2 23108 iscnp2 23143 discmp 23302 2ndcdisj 23360 ptunimpt 23499 pttopon 23500 ptcnplem 23525 upxp 23527 txdis1cn 23539 cnmpt11 23567 cnmpt21 23575 cnmptkp 23584 cnmptk1 23585 cnmpt1k 23586 cnmptkk 23587 cnmptk1p 23589 qtopeu 23620 uzrest 23801 txflf 23910 clsnsg 24014 tgpconncomp 24017 tsmsf1o 24049 prdsmet 24275 fsumcn 24778 cncfmpt1f 24824 iccpnfcnv 24859 lebnumlem1 24877 copco 24935 pcoass 24941 bcth3 25248 voliun 25472 i1f1lem 25607 iblcnlem 25707 limcvallem 25789 ellimc2 25795 cnmptlimc 25808 dvle 25929 dvfsumle 25943 dvfsumleOLD 25944 dvfsumge 25945 dvfsumabs 25946 dvfsumlem2 25950 dvfsumlem2OLD 25951 itgsubstlem 25972 sincn 26371 coscn 26372 rlimcxp 26901 harmonicbnd 26931 harmonicbnd2 26932 lgamgulmlem6 26961 sqff1o 27109 lgseisenlem3 27305 fmptdF 32618 ordtrest2NEW 33909 ddemeas 34222 eulerpartgbij 34359 0rrv 34438 reprpmtf1o 34613 subfacf 35167 tailf 36368 fdc 37744 heiborlem5 37814 3factsumint 42018 dvle2 42065 fmpocos 42227 elrfirn2 42689 mptfcl 42713 mzpexpmpt 42738 mzpsubst 42741 rabdiophlem1 42794 rabdiophlem2 42795 pw2f1ocnv 43030 refsumcn 45028 fmptf 45237 fmptff 45267 fprodcnlem 45600 dvsinax 45914 itgsubsticclem 45976 fargshiftf 47444

W3C validator