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 7086

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 6656	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5929	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3124	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2849	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 483	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3158	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 416	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4018	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3972	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6520	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 592	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6709	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6220	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2811	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3446	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 220	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 211	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 ∧ wa 399 = wceq 1559 ∈ wcel 2141 {cab 2739 ∀wral 3075 ∃wrex 3085 {crab 3413 ⊆ wss 3902 ↦ cmpt 5178 ^◡ccnv 5642 ran crn 5644 “ cima 5646 Fn wfn 6511 ⟶wf 6512

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-pr 5387

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-sn 4580 df-pr 4582 df-op 4586 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5538 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-fun 6518 df-fn 6519 df-f 6520

This theorem is referenced by: f1ompt 7087 fmpti 7088 fvmptelcdm 7089 fmptd 7090 fmptdf 7093 fompt 7094 rnmptss 7099 f1oresrab 7104 idref 7123 f1mpt 7240 f1stres 7989 f2ndres 7990 fmpox 8043 fmpoco 8068 onoviun 8308 onnseq 8309 mptelixpg 8911 dom2lem 8967 iinfi 9357 cantnfrescl 9625 acni2 9996 acnlem 9998 dfac4 10072 dfacacn 10092 fin23lem28 10291 axdc2lem 10399 axcclem 10408 ac6num 10430 uzf 12836 ccatalpha 14601 repsf 14780 rlim2 15514 rlimi 15531 o1fsum 15832 ackbijnn 15849 pcmptcl 16918 vdwlem11 17018 ismon2 17758 isepi2 17765 yonedalem3b 18302 smndex1gbasOLD 18928 efgsf 19760 gsummhm2 19970 gsummptcl 19998 gsummptfif1o 19999 gsummptfzcl 20000 gsumcom2 20006 gsummptnn0fz 20017 issrngd 20892 ipcl 21673 subrgasclcl 22108 evl1sca 22385 mavmulcl 22595 m2detleiblem3 22677 m2detleiblem4 22678 iinopn 22950 ordtrest2 23252 iscnp2 23287 discmp 23446 2ndcdisj 23504 ptunimpt 23643 pttopon 23644 ptcnplem 23669 upxp 23671 txdis1cn 23683 cnmpt11 23711 cnmpt21 23719 cnmptkp 23728 cnmptk1 23729 cnmpt1k 23730 cnmptkk 23731 cnmptk1p 23733 qtopeu 23764 uzrest 23945 txflf 24054 clsnsg 24158 tgpconncomp 24161 tsmsf1o 24193 prdsmet 24418 fsumcn 24920 cncfmpt1f 24964 iccpnfcnv 24994 lebnumlem1 25011 copco 25068 pcoass 25074 bcth3 25381 voliun 25604 i1f1lem 25739 iblcnlem 25839 limcvallem 25921 ellimc2 25927 cnmptlimc 25940 dvle 26057 dvfsumle 26071 dvfsumge 26072 dvfsumabs 26073 dvfsumlem2 26077 itgsubstlem 26098 sincn 26495 coscn 26496 rlimcxp 27026 harmonicbnd 27056 harmonicbnd2 27057 lgamgulmlem6 27086 sqff1o 27234 lgseisenlem3 27429 mptelee 29052 fmptdF 32819 ordtrest2NEW 34181 ddemeas 34494 eulerpartgbij 34630 0rrv 34709 reprpmtf1o 34881 subfacf 35486 tailf 36696 fdc 38205 heiborlem5 38275 3factsumint 42603 dvle2 42650 fmpocos 42813 elrfirn2 43238 mptfcl 43262 mzpexpmpt 43287 mzpsubst 43290 rabdiophlem1 43339 rabdiophlem2 43340 pw2f1ocnv 43575 refsumcn 45571 fmptf 45775 fmptff 45805 fprodcnlem 46136 dvsinax 46448 itgsubsticclem 46510 fargshiftf 48007

W3C validator