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 5914	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3101	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2825	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3135	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4021	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3974	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6504	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 584	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6692	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6204	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2787	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3434	. . 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 1542 ∈ wcel 2114 {cab 2715 ∀wral 3052 ∃wrex 3062 {crab 3401 ⊆ wss 3903 ↦ cmpt 5181 ^◡ccnv 5631 ran crn 5633 “ cima 5635 Fn wfn 6495 ⟶wf 6496

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-pr 5379

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-fun 6502 df-fn 6503 df-f 6504

This theorem is referenced by: f1ompt 7065 fmpti 7066 fvmptelcdm 7067 fmptd 7068 fmptdf 7071 fompt 7072 rnmptss 7077 f1oresrab 7082 idref 7101 f1mpt 7217 f1stres 7967 f2ndres 7968 fmpox 8021 fmpoco 8047 onoviun 8285 onnseq 8286 mptelixpg 8885 dom2lem 8941 iinfi 9332 cantnfrescl 9597 acni2 9968 acnlem 9970 dfac4 10044 dfacacn 10064 fin23lem28 10262 axdc2lem 10370 axcclem 10379 ac6num 10401 uzf 12766 ccatalpha 14529 repsf 14708 rlim2 15431 rlimi 15448 o1fsum 15748 ackbijnn 15763 pcmptcl 16831 vdwlem11 16931 ismon2 17670 isepi2 17677 yonedalem3b 18214 smndex1gbas 18839 efgsf 19670 gsummhm2 19880 gsummptcl 19908 gsummptfif1o 19909 gsummptfzcl 19910 gsumcom2 19916 gsummptnn0fz 19927 issrngd 20800 ipcl 21600 subrgasclcl 22034 evl1sca 22290 mavmulcl 22503 m2detleiblem3 22585 m2detleiblem4 22586 iinopn 22858 ordtrest2 23160 iscnp2 23195 discmp 23354 2ndcdisj 23412 ptunimpt 23551 pttopon 23552 ptcnplem 23577 upxp 23579 txdis1cn 23591 cnmpt11 23619 cnmpt21 23627 cnmptkp 23636 cnmptk1 23637 cnmpt1k 23638 cnmptkk 23639 cnmptk1p 23641 qtopeu 23672 uzrest 23853 txflf 23962 clsnsg 24066 tgpconncomp 24069 tsmsf1o 24101 prdsmet 24326 fsumcn 24829 cncfmpt1f 24875 iccpnfcnv 24910 lebnumlem1 24928 copco 24986 pcoass 24992 bcth3 25299 voliun 25523 i1f1lem 25658 iblcnlem 25758 limcvallem 25840 ellimc2 25846 cnmptlimc 25859 dvle 25980 dvfsumle 25994 dvfsumleOLD 25995 dvfsumge 25996 dvfsumabs 25997 dvfsumlem2 26001 dvfsumlem2OLD 26002 itgsubstlem 26023 sincn 26422 coscn 26423 rlimcxp 26952 harmonicbnd 26982 harmonicbnd2 26983 lgamgulmlem6 27012 sqff1o 27160 lgseisenlem3 27356 mptelee 28979 fmptdF 32746 ordtrest2NEW 34101 ddemeas 34414 eulerpartgbij 34550 0rrv 34629 reprpmtf1o 34804 subfacf 35391 tailf 36591 fdc 37996 heiborlem5 38066 3factsumint 42395 dvle2 42442 fmpocos 42606 elrfirn2 43053 mptfcl 43077 mzpexpmpt 43102 mzpsubst 43105 rabdiophlem1 43158 rabdiophlem2 43159 pw2f1ocnv 43394 refsumcn 45390 fmptf 45597 fmptff 45627 fprodcnlem 45959 dvsinax 46271 itgsubsticclem 46333 fargshiftf 47800

W3C validator