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 7130

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 6708	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5968	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3114	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2829	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3151	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4068	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 4022	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6565	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6758	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6258	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2792	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3470	. . 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 2108 {cab 2714 ∀wral 3061 ∃wrex 3070 {crab 3436 ⊆ wss 3951 ↦ cmpt 5225 ^◡ccnv 5684 ran crn 5686 “ cima 5688 Fn wfn 6556 ⟶wf 6557

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-fun 6563 df-fn 6564 df-f 6565

This theorem is referenced by: f1ompt 7131 fmpti 7132 fvmptelcdm 7133 fmptd 7134 fmptdf 7137 fompt 7138 rnmptss 7143 f1oresrab 7147 idref 7166 f1mpt 7281 f1stres 8038 f2ndres 8039 fmpox 8092 fmpoco 8120 onoviun 8383 onnseq 8384 mptelixpg 8975 dom2lem 9032 iinfi 9457 cantnfrescl 9716 acni2 10086 acnlem 10088 dfac4 10162 dfacacn 10182 fin23lem28 10380 axdc2lem 10488 axcclem 10497 ac6num 10519 uzf 12881 ccatalpha 14631 repsf 14811 rlim2 15532 rlimi 15549 o1fsum 15849 ackbijnn 15864 pcmptcl 16929 vdwlem11 17029 ismon2 17778 isepi2 17785 yonedalem3b 18324 smndex1gbas 18915 efgsf 19747 gsummhm2 19957 gsummptcl 19985 gsummptfif1o 19986 gsummptfzcl 19987 gsumcom2 19993 gsummptnn0fz 20004 issrngd 20856 ipcl 21651 subrgasclcl 22091 evl1sca 22338 mavmulcl 22553 m2detleiblem3 22635 m2detleiblem4 22636 iinopn 22908 ordtrest2 23212 iscnp2 23247 discmp 23406 2ndcdisj 23464 ptunimpt 23603 pttopon 23604 ptcnplem 23629 upxp 23631 txdis1cn 23643 cnmpt11 23671 cnmpt21 23679 cnmptkp 23688 cnmptk1 23689 cnmpt1k 23690 cnmptkk 23691 cnmptk1p 23693 qtopeu 23724 uzrest 23905 txflf 24014 clsnsg 24118 tgpconncomp 24121 tsmsf1o 24153 prdsmet 24380 fsumcn 24894 cncfmpt1f 24940 iccpnfcnv 24975 lebnumlem1 24993 copco 25051 pcoass 25057 bcth3 25365 voliun 25589 i1f1lem 25724 iblcnlem 25824 limcvallem 25906 ellimc2 25912 cnmptlimc 25925 dvle 26046 dvfsumle 26060 dvfsumleOLD 26061 dvfsumge 26062 dvfsumabs 26063 dvfsumlem2 26067 dvfsumlem2OLD 26068 itgsubstlem 26089 sincn 26488 coscn 26489 rlimcxp 27017 harmonicbnd 27047 harmonicbnd2 27048 lgamgulmlem6 27077 sqff1o 27225 lgseisenlem3 27421 fmptdF 32666 ordtrest2NEW 33922 ddemeas 34237 eulerpartgbij 34374 0rrv 34453 reprpmtf1o 34641 subfacf 35180 tailf 36376 fdc 37752 heiborlem5 37822 3factsumint 42026 dvle2 42073 fmpocos 42275 elrfirn2 42707 mptfcl 42731 mzpexpmpt 42756 mzpsubst 42759 rabdiophlem1 42812 rabdiophlem2 42813 pw2f1ocnv 43049 refsumcn 45035 fmptf 45245 fmptff 45276 fprodcnlem 45614 dvsinax 45928 itgsubsticclem 45990 fargshiftf 47427

W3C validator