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 7082

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 6658	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5921	. . . 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 4031	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3985	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6515	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6710	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6211	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2779	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3439	. . 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 3405 ⊆ wss 3914 ↦ cmpt 5188 ^◡ccnv 5637 ran crn 5639 “ cima 5641 Fn wfn 6506 ⟶wf 6507

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 5251 ax-nul 5261 ax-pr 5387

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 3406 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-fun 6513 df-fn 6514 df-f 6515

This theorem is referenced by: f1ompt 7083 fmpti 7084 fvmptelcdm 7085 fmptd 7086 fmptdf 7089 fompt 7090 rnmptss 7095 f1oresrab 7099 idref 7118 f1mpt 7236 f1stres 7992 f2ndres 7993 fmpox 8046 fmpoco 8074 onoviun 8312 onnseq 8313 mptelixpg 8908 dom2lem 8963 iinfi 9368 cantnfrescl 9629 acni2 9999 acnlem 10001 dfac4 10075 dfacacn 10095 fin23lem28 10293 axdc2lem 10401 axcclem 10410 ac6num 10432 uzf 12796 ccatalpha 14558 repsf 14738 rlim2 15462 rlimi 15479 o1fsum 15779 ackbijnn 15794 pcmptcl 16862 vdwlem11 16962 ismon2 17696 isepi2 17703 yonedalem3b 18240 smndex1gbas 18829 efgsf 19659 gsummhm2 19869 gsummptcl 19897 gsummptfif1o 19898 gsummptfzcl 19899 gsumcom2 19905 gsummptnn0fz 19916 issrngd 20764 ipcl 21542 subrgasclcl 21974 evl1sca 22221 mavmulcl 22434 m2detleiblem3 22516 m2detleiblem4 22517 iinopn 22789 ordtrest2 23091 iscnp2 23126 discmp 23285 2ndcdisj 23343 ptunimpt 23482 pttopon 23483 ptcnplem 23508 upxp 23510 txdis1cn 23522 cnmpt11 23550 cnmpt21 23558 cnmptkp 23567 cnmptk1 23568 cnmpt1k 23569 cnmptkk 23570 cnmptk1p 23572 qtopeu 23603 uzrest 23784 txflf 23893 clsnsg 23997 tgpconncomp 24000 tsmsf1o 24032 prdsmet 24258 fsumcn 24761 cncfmpt1f 24807 iccpnfcnv 24842 lebnumlem1 24860 copco 24918 pcoass 24924 bcth3 25231 voliun 25455 i1f1lem 25590 iblcnlem 25690 limcvallem 25772 ellimc2 25778 cnmptlimc 25791 dvle 25912 dvfsumle 25926 dvfsumleOLD 25927 dvfsumge 25928 dvfsumabs 25929 dvfsumlem2 25933 dvfsumlem2OLD 25934 itgsubstlem 25955 sincn 26354 coscn 26355 rlimcxp 26884 harmonicbnd 26914 harmonicbnd2 26915 lgamgulmlem6 26944 sqff1o 27092 lgseisenlem3 27288 fmptdF 32580 ordtrest2NEW 33913 ddemeas 34226 eulerpartgbij 34363 0rrv 34442 reprpmtf1o 34617 subfacf 35162 tailf 36363 fdc 37739 heiborlem5 37809 3factsumint 42013 dvle2 42060 fmpocos 42222 elrfirn2 42684 mptfcl 42708 mzpexpmpt 42733 mzpsubst 42736 rabdiophlem1 42789 rabdiophlem2 42790 pw2f1ocnv 43026 refsumcn 45024 fmptf 45233 fmptff 45263 fprodcnlem 45597 dvsinax 45911 itgsubsticclem 45973 fargshiftf 47441

W3C validator