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 6703

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 6323	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5675	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3202	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2855	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 472	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3229	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 405	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 3937	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	syl5eqss 3907	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6197	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 575	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14	1	mptpreima 5936	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
15		fimacnv 6670	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
16	14, 15	syl5reqr 2831	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3322	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 210	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 201	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 198 ∧ wa 387 = wceq 1508 ∈ wcel 2051 {cab 2760 ∀wral 3090 ∃wrex 3091 {crab 3094 ⊆ wss 3831 ↦ cmpt 5013 ^◡ccnv 5410 ran crn 5412 “ cima 5414 Fn wfn 6188 ⟶wf 6189

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2752 ax-sep 5064 ax-nul 5071 ax-pr 5190

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2551 df-eu 2589 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3419 df-sbc 3684 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4182 df-if 4354 df-sn 4445 df-pr 4447 df-op 4451 df-uni 4718 df-br 4935 df-opab 4997 df-mpt 5014 df-id 5316 df-xp 5417 df-rel 5418 df-cnv 5419 df-co 5420 df-dm 5421 df-rn 5422 df-res 5423 df-ima 5424 df-iota 6157 df-fun 6195 df-fn 6196 df-f 6197 df-fv 6201

This theorem is referenced by: f1ompt 6704 fmpti 6705 fvmptelrn 6706 fmptd 6707 fmptdf 6710 rnmptss 6715 f1oresrab 6718 idref 6737 f1mpt 6850 f1stres 7531 f2ndres 7532 fmpox 7579 fmpoco 7604 onoviun 7790 onnseq 7791 mptelixpg 8302 dom2lem 8352 iinfi 8682 cantnfrescl 8939 acni2 9272 acnlem 9274 dfac4 9348 dfacacn 9367 fin23lem28 9566 axdc2lem 9674 axcclem 9683 ac6num 9705 uzf 12067 ccatalpha 13762 repsf 13998 rlim2 14720 rlimi 14737 o1fsum 15034 ackbijnn 15049 pcmptcl 16089 vdwlem11 16189 ismon2 16874 isepi2 16881 yonedalem3b 17399 efgsf 18625 gsummhm2 18824 gsummptcl 18852 gsummptfif1o 18853 gsummptfzcl 18854 gsumcom2 18860 gsummptnn0fz 18868 issrngd 19366 subrgasclcl 20004 evl1sca 20214 ipcl 20494 mavmulcl 20875 m2detleiblem3 20957 m2detleiblem4 20958 iinopn 21229 ordtrest2 21531 iscnp2 21566 discmp 21725 2ndcdisj 21783 ptunimpt 21922 pttopon 21923 ptcnplem 21948 upxp 21950 txdis1cn 21962 cnmpt11 21990 cnmpt21 21998 cnmptkp 22007 cnmptk1 22008 cnmpt1k 22009 cnmptkk 22010 cnmptk1p 22012 qtopeu 22043 uzrest 22224 txflf 22333 clsnsg 22436 tgpconncomp 22439 tsmsf1o 22471 prdsmet 22698 fsumcn 23196 cncfmpt1f 23239 iccpnfcnv 23266 lebnumlem1 23283 copco 23340 pcoass 23346 bcth3 23652 voliun 23873 i1f1lem 24008 iblcnlem 24107 limcvallem 24187 ellimc2 24193 cnmptlimc 24206 dvle 24322 dvfsumle 24336 dvfsumge 24337 dvfsumabs 24338 dvfsumlem2 24342 itgsubstlem 24363 sincn 24750 coscn 24751 rlimcxp 25268 harmonicbnd 25298 harmonicbnd2 25299 lgamgulmlem6 25328 sqff1o 25476 lgseisenlem3 25670 fmptdF 30180 ordtrest2NEW 30842 ddemeas 31172 eulerpartgbij 31307 0rrv 31387 reprpmtf1o 31577 subfacf 32047 tailf 33284 fdc 34502 heiborlem5 34575 elrfirn2 38729 mptfcl 38753 mzpexpmpt 38778 mzpsubst 38781 rabdiophlem1 38835 rabdiophlem2 38836 pw2f1ocnv 39071 refsumcn 40746 fompt 40914 fmptf 40972 fprodcnlem 41346 dvsinax 41662 itgsubsticclem 41725 fargshiftf 43007 isomuspgrlem2b 43397

W3C validator