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 7064

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 6640	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5910	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3094	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2816	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3130	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4028	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3982	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6503	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6692	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6199	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2779	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3436	. . 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 3402 ⊆ wss 3911 ↦ cmpt 5183 ^◡ccnv 5630 ran crn 5632 “ cima 5634 Fn wfn 6494 ⟶wf 6495

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 5246 ax-nul 5256 ax-pr 5382

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 3403 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-fun 6501 df-fn 6502 df-f 6503

This theorem is referenced by: f1ompt 7065 fmpti 7066 fvmptelcdm 7067 fmptd 7068 fmptdf 7071 fompt 7072 rnmptss 7077 f1oresrab 7081 idref 7100 f1mpt 7218 f1stres 7971 f2ndres 7972 fmpox 8025 fmpoco 8051 onoviun 8289 onnseq 8290 mptelixpg 8885 dom2lem 8940 iinfi 9344 cantnfrescl 9605 acni2 9975 acnlem 9977 dfac4 10051 dfacacn 10071 fin23lem28 10269 axdc2lem 10377 axcclem 10386 ac6num 10408 uzf 12772 ccatalpha 14534 repsf 14714 rlim2 15438 rlimi 15455 o1fsum 15755 ackbijnn 15770 pcmptcl 16838 vdwlem11 16938 ismon2 17672 isepi2 17679 yonedalem3b 18216 smndex1gbas 18805 efgsf 19635 gsummhm2 19845 gsummptcl 19873 gsummptfif1o 19874 gsummptfzcl 19875 gsumcom2 19881 gsummptnn0fz 19892 issrngd 20740 ipcl 21518 subrgasclcl 21950 evl1sca 22197 mavmulcl 22410 m2detleiblem3 22492 m2detleiblem4 22493 iinopn 22765 ordtrest2 23067 iscnp2 23102 discmp 23261 2ndcdisj 23319 ptunimpt 23458 pttopon 23459 ptcnplem 23484 upxp 23486 txdis1cn 23498 cnmpt11 23526 cnmpt21 23534 cnmptkp 23543 cnmptk1 23544 cnmpt1k 23545 cnmptkk 23546 cnmptk1p 23548 qtopeu 23579 uzrest 23760 txflf 23869 clsnsg 23973 tgpconncomp 23976 tsmsf1o 24008 prdsmet 24234 fsumcn 24737 cncfmpt1f 24783 iccpnfcnv 24818 lebnumlem1 24836 copco 24894 pcoass 24900 bcth3 25207 voliun 25431 i1f1lem 25566 iblcnlem 25666 limcvallem 25748 ellimc2 25754 cnmptlimc 25767 dvle 25888 dvfsumle 25902 dvfsumleOLD 25903 dvfsumge 25904 dvfsumabs 25905 dvfsumlem2 25909 dvfsumlem2OLD 25910 itgsubstlem 25931 sincn 26330 coscn 26331 rlimcxp 26860 harmonicbnd 26890 harmonicbnd2 26891 lgamgulmlem6 26920 sqff1o 27068 lgseisenlem3 27264 fmptdF 32553 ordtrest2NEW 33886 ddemeas 34199 eulerpartgbij 34336 0rrv 34415 reprpmtf1o 34590 subfacf 35135 tailf 36336 fdc 37712 heiborlem5 37782 3factsumint 41986 dvle2 42033 fmpocos 42195 elrfirn2 42657 mptfcl 42681 mzpexpmpt 42706 mzpsubst 42709 rabdiophlem1 42762 rabdiophlem2 42763 pw2f1ocnv 42999 refsumcn 44997 fmptf 45206 fmptff 45236 fprodcnlem 45570 dvsinax 45884 itgsubsticclem 45946 fargshiftf 47414

W3C validator