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 7106

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 6687	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5952	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3114	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2821	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 480	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3151	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 413	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4064	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 4029	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6544	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6736	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6234	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2787	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3464	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 217	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2709 ∀wral 3061 ∃wrex 3070 {crab 3432 ⊆ wss 3947 ↦ cmpt 5230 ^◡ccnv 5674 ran crn 5676 “ cima 5678 Fn wfn 6535 ⟶wf 6536

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-fun 6542 df-fn 6543 df-f 6544

This theorem is referenced by: f1ompt 7107 fmpti 7108 fvmptelcdm 7109 fmptd 7110 fmptdf 7113 rnmptss 7118 f1oresrab 7121 idref 7140 f1mpt 7256 f1stres 7995 f2ndres 7996 fmpox 8049 fmpoco 8077 onoviun 8339 onnseq 8340 mptelixpg 8925 dom2lem 8984 iinfi 9408 cantnfrescl 9667 acni2 10037 acnlem 10039 dfac4 10113 dfacacn 10132 fin23lem28 10331 axdc2lem 10439 axcclem 10448 ac6num 10470 uzf 12821 ccatalpha 14539 repsf 14719 rlim2 15436 rlimi 15453 o1fsum 15755 ackbijnn 15770 pcmptcl 16820 vdwlem11 16920 ismon2 17677 isepi2 17684 yonedalem3b 18228 smndex1gbas 18779 efgsf 19591 gsummhm2 19801 gsummptcl 19829 gsummptfif1o 19830 gsummptfzcl 19831 gsumcom2 19837 gsummptnn0fz 19848 issrngd 20461 ipcl 21177 subrgasclcl 21619 evl1sca 21844 mavmulcl 22040 m2detleiblem3 22122 m2detleiblem4 22123 iinopn 22395 ordtrest2 22699 iscnp2 22734 discmp 22893 2ndcdisj 22951 ptunimpt 23090 pttopon 23091 ptcnplem 23116 upxp 23118 txdis1cn 23130 cnmpt11 23158 cnmpt21 23166 cnmptkp 23175 cnmptk1 23176 cnmpt1k 23177 cnmptkk 23178 cnmptk1p 23180 qtopeu 23211 uzrest 23392 txflf 23501 clsnsg 23605 tgpconncomp 23608 tsmsf1o 23640 prdsmet 23867 fsumcn 24377 cncfmpt1f 24421 iccpnfcnv 24451 lebnumlem1 24468 copco 24525 pcoass 24531 bcth3 24839 voliun 25062 i1f1lem 25197 iblcnlem 25297 limcvallem 25379 ellimc2 25385 cnmptlimc 25398 dvle 25515 dvfsumle 25529 dvfsumge 25530 dvfsumabs 25531 dvfsumlem2 25535 itgsubstlem 25556 sincn 25947 coscn 25948 rlimcxp 26467 harmonicbnd 26497 harmonicbnd2 26498 lgamgulmlem6 26527 sqff1o 26675 lgseisenlem3 26869 fmptdF 31868 ordtrest2NEW 32891 ddemeas 33222 eulerpartgbij 33359 0rrv 33438 reprpmtf1o 33626 subfacf 34154 gg-dvfsumle 35170 gg-dvfsumlem2 35171 tailf 35248 fdc 36601 heiborlem5 36671 3factsumint 40878 dvle2 40925 fmpocos 41053 elrfirn2 41419 mptfcl 41443 mzpexpmpt 41468 mzpsubst 41471 rabdiophlem1 41524 rabdiophlem2 41525 pw2f1ocnv 41761 refsumcn 43699 fompt 43875 fmptf 43927 fmptff 43960 fprodcnlem 44301 dvsinax 44615 itgsubsticclem 44677 fargshiftf 46094 isomuspgrlem2b 46483

W3C validator