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 7049

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 6626	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5901	. . . 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 6490	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6678	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6190	. . . 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 5174 ^◡ccnv 5618 ran crn 5620 “ cima 5622 Fn wfn 6481 ⟶wf 6482

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 5236 ax-nul 5246 ax-pr 5372

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 4475 df-sn 4576 df-pr 4578 df-op 4582 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-fun 6488 df-fn 6489 df-f 6490

This theorem is referenced by: f1ompt 7050 fmpti 7051 fvmptelcdm 7052 fmptd 7053 fmptdf 7056 fompt 7057 rnmptss 7062 f1oresrab 7066 idref 7085 f1mpt 7201 f1stres 7951 f2ndres 7952 fmpox 8005 fmpoco 8031 onoviun 8269 onnseq 8270 mptelixpg 8865 dom2lem 8921 iinfi 9308 cantnfrescl 9573 acni2 9944 acnlem 9946 dfac4 10020 dfacacn 10040 fin23lem28 10238 axdc2lem 10346 axcclem 10355 ac6num 10377 uzf 12741 ccatalpha 14503 repsf 14682 rlim2 15405 rlimi 15422 o1fsum 15722 ackbijnn 15737 pcmptcl 16805 vdwlem11 16905 ismon2 17643 isepi2 17650 yonedalem3b 18187 smndex1gbas 18812 efgsf 19643 gsummhm2 19853 gsummptcl 19881 gsummptfif1o 19882 gsummptfzcl 19883 gsumcom2 19889 gsummptnn0fz 19900 issrngd 20772 ipcl 21572 subrgasclcl 22003 evl1sca 22250 mavmulcl 22463 m2detleiblem3 22545 m2detleiblem4 22546 iinopn 22818 ordtrest2 23120 iscnp2 23155 discmp 23314 2ndcdisj 23372 ptunimpt 23511 pttopon 23512 ptcnplem 23537 upxp 23539 txdis1cn 23551 cnmpt11 23579 cnmpt21 23587 cnmptkp 23596 cnmptk1 23597 cnmpt1k 23598 cnmptkk 23599 cnmptk1p 23601 qtopeu 23632 uzrest 23813 txflf 23922 clsnsg 24026 tgpconncomp 24029 tsmsf1o 24061 prdsmet 24286 fsumcn 24789 cncfmpt1f 24835 iccpnfcnv 24870 lebnumlem1 24888 copco 24946 pcoass 24952 bcth3 25259 voliun 25483 i1f1lem 25618 iblcnlem 25718 limcvallem 25800 ellimc2 25806 cnmptlimc 25819 dvle 25940 dvfsumle 25954 dvfsumleOLD 25955 dvfsumge 25956 dvfsumabs 25957 dvfsumlem2 25961 dvfsumlem2OLD 25962 itgsubstlem 25983 sincn 26382 coscn 26383 rlimcxp 26912 harmonicbnd 26942 harmonicbnd2 26943 lgamgulmlem6 26972 sqff1o 27120 lgseisenlem3 27316 mptelee 28874 fmptdF 32640 ordtrest2NEW 33957 ddemeas 34270 eulerpartgbij 34406 0rrv 34485 reprpmtf1o 34660 subfacf 35240 tailf 36440 fdc 37805 heiborlem5 37875 3factsumint 42138 dvle2 42185 fmpocos 42352 elrfirn2 42813 mptfcl 42837 mzpexpmpt 42862 mzpsubst 42865 rabdiophlem1 42918 rabdiophlem2 42919 pw2f1ocnv 43154 refsumcn 45151 fmptf 45360 fmptff 45390 fprodcnlem 45723 dvsinax 46035 itgsubsticclem 46097 fargshiftf 47564

W3C validator