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 7051

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 6625	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5899	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3102	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2827	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 480	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3136	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 413	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 3998	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3953	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6489	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 589	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6677	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6189	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2789	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3424	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 219	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 210	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 {cab 2717 ∀wral 3053 ∃wrex 3063 {crab 3391 ⊆ wss 3883 ↦ cmpt 5153 ^◡ccnv 5617 ran crn 5619 “ cima 5621 Fn wfn 6480 ⟶wf 6481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-pr 5362

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-sn 4556 df-pr 4558 df-op 4562 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-fun 6487 df-fn 6488 df-f 6489

This theorem is referenced by: f1ompt 7052 fmpti 7053 fvmptelcdm 7054 fmptd 7055 fmptdf 7058 fompt 7059 rnmptss 7064 f1oresrab 7069 idref 7088 f1mpt 7205 f1stres 7955 f2ndres 7956 fmpox 8009 fmpoco 8034 onoviun 8273 onnseq 8274 mptelixpg 8873 dom2lem 8929 iinfi 9320 cantnfrescl 9588 acni2 9959 acnlem 9961 dfac4 10035 dfacacn 10055 fin23lem28 10253 axdc2lem 10361 axcclem 10370 ac6num 10392 uzf 12782 ccatalpha 14547 repsf 14726 rlim2 15449 rlimi 15466 o1fsum 15767 ackbijnn 15784 pcmptcl 16853 vdwlem11 16953 ismon2 17692 isepi2 17699 yonedalem3b 18236 smndex1gbasOLD 18862 efgsf 19695 gsummhm2 19905 gsummptcl 19933 gsummptfif1o 19934 gsummptfzcl 19935 gsumcom2 19941 gsummptnn0fz 19952 issrngd 20827 ipcl 21608 subrgasclcl 22043 evl1sca 22320 mavmulcl 22530 m2detleiblem3 22612 m2detleiblem4 22613 iinopn 22885 ordtrest2 23187 iscnp2 23222 discmp 23381 2ndcdisj 23439 ptunimpt 23578 pttopon 23579 ptcnplem 23604 upxp 23606 txdis1cn 23618 cnmpt11 23646 cnmpt21 23654 cnmptkp 23663 cnmptk1 23664 cnmpt1k 23665 cnmptkk 23666 cnmptk1p 23668 qtopeu 23699 uzrest 23880 txflf 23989 clsnsg 24093 tgpconncomp 24096 tsmsf1o 24128 prdsmet 24353 fsumcn 24855 cncfmpt1f 24899 iccpnfcnv 24929 lebnumlem1 24946 copco 25003 pcoass 25009 bcth3 25316 voliun 25539 i1f1lem 25674 iblcnlem 25774 limcvallem 25856 ellimc2 25862 cnmptlimc 25875 dvle 25992 dvfsumle 26006 dvfsumge 26007 dvfsumabs 26008 dvfsumlem2 26012 itgsubstlem 26033 sincn 26427 coscn 26428 rlimcxp 26955 harmonicbnd 26985 harmonicbnd2 26986 lgamgulmlem6 27015 sqff1o 27163 lgseisenlem3 27358 mptelee 28981 fmptdF 32748 ordtrest2NEW 34107 ddemeas 34420 eulerpartgbij 34556 0rrv 34635 reprpmtf1o 34810 subfacf 35403 tailf 36603 fdc 38112 heiborlem5 38182 3factsumint 42510 dvle2 42557 fmpocos 42720 elrfirn2 43145 mptfcl 43169 mzpexpmpt 43194 mzpsubst 43197 rabdiophlem1 43246 rabdiophlem2 43247 pw2f1ocnv 43482 refsumcn 45478 fmptf 45683 fmptff 45713 fprodcnlem 46044 dvsinax 46356 itgsubsticclem 46418 fargshiftf 47915

W3C validator