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 7052

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 6629	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5903	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3096	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2821	. . . . . . . . 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 4016	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3969	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6493	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6681	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6193	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2783	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3429	. . 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 1541 ∈ wcel 2113 {cab 2711 ∀wral 3048 ∃wrex 3057 {crab 3396 ⊆ wss 3898 ↦ cmpt 5176 ^◡ccnv 5620 ran crn 5622 “ cima 5624 Fn wfn 6484 ⟶wf 6485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pr 5374

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-fun 6491 df-fn 6492 df-f 6493

This theorem is referenced by: f1ompt 7053 fmpti 7054 fvmptelcdm 7055 fmptd 7056 fmptdf 7059 fompt 7060 rnmptss 7065 f1oresrab 7069 idref 7088 f1mpt 7204 f1stres 7954 f2ndres 7955 fmpox 8008 fmpoco 8034 onoviun 8272 onnseq 8273 mptelixpg 8869 dom2lem 8925 iinfi 9312 cantnfrescl 9577 acni2 9948 acnlem 9950 dfac4 10024 dfacacn 10044 fin23lem28 10242 axdc2lem 10350 axcclem 10359 ac6num 10381 uzf 12745 ccatalpha 14508 repsf 14687 rlim2 15410 rlimi 15427 o1fsum 15727 ackbijnn 15742 pcmptcl 16810 vdwlem11 16910 ismon2 17649 isepi2 17656 yonedalem3b 18193 smndex1gbas 18818 efgsf 19649 gsummhm2 19859 gsummptcl 19887 gsummptfif1o 19888 gsummptfzcl 19889 gsumcom2 19895 gsummptnn0fz 19906 issrngd 20779 ipcl 21579 subrgasclcl 22013 evl1sca 22269 mavmulcl 22482 m2detleiblem3 22564 m2detleiblem4 22565 iinopn 22837 ordtrest2 23139 iscnp2 23174 discmp 23333 2ndcdisj 23391 ptunimpt 23530 pttopon 23531 ptcnplem 23556 upxp 23558 txdis1cn 23570 cnmpt11 23598 cnmpt21 23606 cnmptkp 23615 cnmptk1 23616 cnmpt1k 23617 cnmptkk 23618 cnmptk1p 23620 qtopeu 23651 uzrest 23832 txflf 23941 clsnsg 24045 tgpconncomp 24048 tsmsf1o 24080 prdsmet 24305 fsumcn 24808 cncfmpt1f 24854 iccpnfcnv 24889 lebnumlem1 24907 copco 24965 pcoass 24971 bcth3 25278 voliun 25502 i1f1lem 25637 iblcnlem 25737 limcvallem 25819 ellimc2 25825 cnmptlimc 25838 dvle 25959 dvfsumle 25973 dvfsumleOLD 25974 dvfsumge 25975 dvfsumabs 25976 dvfsumlem2 25980 dvfsumlem2OLD 25981 itgsubstlem 26002 sincn 26401 coscn 26402 rlimcxp 26931 harmonicbnd 26961 harmonicbnd2 26962 lgamgulmlem6 26991 sqff1o 27139 lgseisenlem3 27335 mptelee 28893 fmptdF 32660 ordtrest2NEW 34008 ddemeas 34321 eulerpartgbij 34457 0rrv 34536 reprpmtf1o 34711 subfacf 35291 tailf 36491 fdc 37858 heiborlem5 37928 3factsumint 42191 dvle2 42238 fmpocos 42405 elrfirn2 42853 mptfcl 42877 mzpexpmpt 42902 mzpsubst 42905 rabdiophlem1 42958 rabdiophlem2 42959 pw2f1ocnv 43194 refsumcn 45191 fmptf 45399 fmptff 45429 fprodcnlem 45761 dvsinax 46073 itgsubsticclem 46135 fargshiftf 47602

W3C validator