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 7129

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 6708	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5970	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3111	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2826	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3148	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4077	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 4043	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6566	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6758	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6259	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2789	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3467	. . 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 1536 ∈ wcel 2105 {cab 2711 ∀wral 3058 ∃wrex 3067 {crab 3432 ⊆ wss 3962 ↦ cmpt 5230 ^◡ccnv 5687 ran crn 5689 “ cima 5691 Fn wfn 6557 ⟶wf 6558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-fun 6564 df-fn 6565 df-f 6566

This theorem is referenced by: f1ompt 7130 fmpti 7131 fvmptelcdm 7132 fmptd 7133 fmptdf 7136 fompt 7137 rnmptss 7142 f1oresrab 7146 idref 7165 f1mpt 7280 f1stres 8036 f2ndres 8037 fmpox 8090 fmpoco 8118 onoviun 8381 onnseq 8382 mptelixpg 8973 dom2lem 9030 iinfi 9454 cantnfrescl 9713 acni2 10083 acnlem 10085 dfac4 10159 dfacacn 10179 fin23lem28 10377 axdc2lem 10485 axcclem 10494 ac6num 10516 uzf 12878 ccatalpha 14627 repsf 14807 rlim2 15528 rlimi 15545 o1fsum 15845 ackbijnn 15860 pcmptcl 16924 vdwlem11 17024 ismon2 17781 isepi2 17788 yonedalem3b 18335 smndex1gbas 18927 efgsf 19761 gsummhm2 19971 gsummptcl 19999 gsummptfif1o 20000 gsummptfzcl 20001 gsumcom2 20007 gsummptnn0fz 20018 issrngd 20872 ipcl 21668 subrgasclcl 22108 evl1sca 22353 mavmulcl 22568 m2detleiblem3 22650 m2detleiblem4 22651 iinopn 22923 ordtrest2 23227 iscnp2 23262 discmp 23421 2ndcdisj 23479 ptunimpt 23618 pttopon 23619 ptcnplem 23644 upxp 23646 txdis1cn 23658 cnmpt11 23686 cnmpt21 23694 cnmptkp 23703 cnmptk1 23704 cnmpt1k 23705 cnmptkk 23706 cnmptk1p 23708 qtopeu 23739 uzrest 23920 txflf 24029 clsnsg 24133 tgpconncomp 24136 tsmsf1o 24168 prdsmet 24395 fsumcn 24907 cncfmpt1f 24953 iccpnfcnv 24988 lebnumlem1 25006 copco 25064 pcoass 25070 bcth3 25378 voliun 25602 i1f1lem 25737 iblcnlem 25838 limcvallem 25920 ellimc2 25926 cnmptlimc 25939 dvle 26060 dvfsumle 26074 dvfsumleOLD 26075 dvfsumge 26076 dvfsumabs 26077 dvfsumlem2 26081 dvfsumlem2OLD 26082 itgsubstlem 26103 sincn 26502 coscn 26503 rlimcxp 27031 harmonicbnd 27061 harmonicbnd2 27062 lgamgulmlem6 27091 sqff1o 27239 lgseisenlem3 27435 fmptdF 32672 ordtrest2NEW 33883 ddemeas 34216 eulerpartgbij 34353 0rrv 34432 reprpmtf1o 34619 subfacf 35159 tailf 36357 fdc 37731 heiborlem5 37801 3factsumint 42006 dvle2 42053 fmpocos 42253 elrfirn2 42683 mptfcl 42707 mzpexpmpt 42732 mzpsubst 42735 rabdiophlem1 42788 rabdiophlem2 42789 pw2f1ocnv 43025 refsumcn 44967 fmptf 45182 fmptff 45214 fprodcnlem 45554 dvsinax 45868 itgsubsticclem 45930 fargshiftf 47364

W3C validator