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 6381

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 6020	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5371	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3072	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2689	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 504	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3029	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 450	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 3676	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	syl5eqss 3649	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 5892	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 698	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14	1	mptpreima 5628	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
15		fimacnv 6347	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
16	14, 15	syl5reqr 2671	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3118	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 208	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 199	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 {cab 2608 ∀wral 2912 ∃wrex 2913 {crab 2916 ⊆ wss 3574 ↦ cmpt 4729 ^◡ccnv 5113 ran crn 5115 “ cima 5117 Fn wfn 5883 ⟶wf 5884

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-fv 5896

This theorem is referenced by: f1ompt 6382 fmpti 6383 mptex2 6384 fmptd 6385 fmptdf 6387 rnmptss 6392 f1oresrab 6395 idref 6499 f1mpt 6518 f1stres 7190 f2ndres 7191 fmpt2x 7236 fmpt2co 7260 onoviun 7440 onnseq 7441 mptelixpg 7945 dom2lem 7995 iinfi 8323 cantnfrescl 8573 acni2 8869 acnlem 8871 dfac4 8945 dfacacn 8963 fin23lem28 9162 axdc2lem 9270 axcclem 9279 ac6num 9301 uzf 11690 ccatalpha 13375 repsf 13520 rlim2 14227 rlimi 14244 rlimmptrcl 14338 lo1mptrcl 14352 o1mptrcl 14353 o1fsum 14545 ackbijnn 14560 pcmptcl 15595 vdwlem11 15695 ismon2 16394 isepi2 16401 yonedalem3b 16919 efgsf 18142 gsummhm2 18339 gsummptcl 18366 gsummptfif1o 18367 gsummptfzcl 18368 gsumcom2 18374 gsummptnn0fz 18382 issrngd 18861 psrass1lem 19377 subrgasclcl 19499 evl1sca 19698 ipcl 19978 frlmgsum 20111 uvcresum 20132 mavmulcl 20353 m2detleiblem3 20435 m2detleiblem4 20436 iinopn 20707 ordtrest2 21008 iscnp2 21043 discmp 21201 2ndcdisj 21259 ptunimpt 21398 pttopon 21399 txcnp 21423 ptcnplem 21424 ptcnp 21425 upxp 21426 ptcn 21430 txdis1cn 21438 cnmpt11 21466 cnmpt1t 21468 cnmpt12 21470 cnmpt21 21474 cnmptkp 21483 cnmptk1 21484 cnmpt1k 21485 cnmptkk 21486 cnmptk1p 21488 cnmptk2 21489 qtopeu 21519 uzrest 21701 txflf 21810 cnmpt1plusg 21891 clsnsg 21913 tgpconncomp 21916 tsmsf1o 21948 cnmpt1vsca 21997 prdsmet 22175 cnmpt1ds 22645 fsumcn 22673 cncfmpt1f 22716 cncfmpt2ss 22718 iccpnfcnv 22743 lebnumlem1 22760 copco 22818 pcoass 22824 cnmpt1ip 23046 bcth3 23128 voliun 23322 mbfmptcl 23404 i1f1lem 23456 i1fposd 23474 iblcnlem 23555 itgss3 23581 limcvallem 23635 ellimc2 23641 cnmptlimc 23654 dvmptcl 23722 dvmptco 23735 dvle 23770 dvfsumle 23784 dvfsumge 23785 dvfsumabs 23786 dvmptrecl 23787 dvfsumlem2 23790 itgparts 23810 itgsubstlem 23811 itgsubst 23812 ulmss 24151 ulmdvlem2 24155 itgulm2 24163 sincn 24198 coscn 24199 logtayl 24406 rlimcxp 24700 harmonicbnd 24730 harmonicbnd2 24731 lgamgulmlem6 24760 sqff1o 24908 lgseisenlem3 25102 fmptdF 29456 ordtrest2NEW 29969 ddemeas 30299 eulerpartgbij 30434 0rrv 30513 reprpmtf1o 30704 subfacf 31157 tailf 32370 fdc 33541 heiborlem5 33614 elrfirn2 37259 mptfcl 37283 mzpexpmpt 37308 mzpsubst 37311 rabdiophlem1 37365 rabdiophlem2 37366 pw2f1ocnv 37604 refsumcn 39189 fompt 39379 fvmptelrn 39428 fmptf 39448 fprodcnlem 39831 dvsinax 40127 itgsubsticclem 40191 fargshiftf 41376

W3C validator