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 7062

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 6638	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5912	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3100	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2824	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3134	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4007	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3960	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6502	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 584	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6690	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6202	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2786	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3422	. . 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 2714 ∀wral 3051 ∃wrex 3061 {crab 3389 ⊆ wss 3889 ↦ cmpt 5166 ^◡ccnv 5630 ran crn 5632 “ cima 5634 Fn wfn 6493 ⟶wf 6494

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 2708 ax-sep 5231 ax-pr 5375

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ral 3052 df-rex 3062 df-rab 3390 df-v 3431 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-sn 4568 df-pr 4570 df-op 4574 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-fun 6500 df-fn 6501 df-f 6502

This theorem is referenced by: f1ompt 7063 fmpti 7064 fvmptelcdm 7065 fmptd 7066 fmptdf 7069 fompt 7070 rnmptss 7075 f1oresrab 7080 idref 7099 f1mpt 7216 f1stres 7966 f2ndres 7967 fmpox 8020 fmpoco 8045 onoviun 8283 onnseq 8284 mptelixpg 8883 dom2lem 8939 iinfi 9330 cantnfrescl 9597 acni2 9968 acnlem 9970 dfac4 10044 dfacacn 10064 fin23lem28 10262 axdc2lem 10370 axcclem 10379 ac6num 10401 uzf 12791 ccatalpha 14556 repsf 14735 rlim2 15458 rlimi 15475 o1fsum 15776 ackbijnn 15793 pcmptcl 16862 vdwlem11 16962 ismon2 17701 isepi2 17708 yonedalem3b 18245 smndex1gbasOLD 18871 efgsf 19704 gsummhm2 19914 gsummptcl 19942 gsummptfif1o 19943 gsummptfzcl 19944 gsumcom2 19950 gsummptnn0fz 19961 issrngd 20832 ipcl 21613 subrgasclcl 22045 evl1sca 22299 mavmulcl 22512 m2detleiblem3 22594 m2detleiblem4 22595 iinopn 22867 ordtrest2 23169 iscnp2 23204 discmp 23363 2ndcdisj 23421 ptunimpt 23560 pttopon 23561 ptcnplem 23586 upxp 23588 txdis1cn 23600 cnmpt11 23628 cnmpt21 23636 cnmptkp 23645 cnmptk1 23646 cnmpt1k 23647 cnmptkk 23648 cnmptk1p 23650 qtopeu 23681 uzrest 23862 txflf 23971 clsnsg 24075 tgpconncomp 24078 tsmsf1o 24110 prdsmet 24335 fsumcn 24837 cncfmpt1f 24881 iccpnfcnv 24911 lebnumlem1 24928 copco 24985 pcoass 24991 bcth3 25298 voliun 25521 i1f1lem 25656 iblcnlem 25756 limcvallem 25838 ellimc2 25844 cnmptlimc 25857 dvle 25974 dvfsumle 25988 dvfsumge 25989 dvfsumabs 25990 dvfsumlem2 25994 itgsubstlem 26015 sincn 26409 coscn 26410 rlimcxp 26937 harmonicbnd 26967 harmonicbnd2 26968 lgamgulmlem6 26997 sqff1o 27145 lgseisenlem3 27340 mptelee 28963 fmptdF 32729 ordtrest2NEW 34067 ddemeas 34380 eulerpartgbij 34516 0rrv 34595 reprpmtf1o 34770 subfacf 35357 tailf 36557 fdc 38066 heiborlem5 38136 3factsumint 42464 dvle2 42511 fmpocos 42675 elrfirn2 43128 mptfcl 43152 mzpexpmpt 43177 mzpsubst 43180 rabdiophlem1 43229 rabdiophlem2 43230 pw2f1ocnv 43465 refsumcn 45461 fmptf 45668 fmptff 45698 fprodcnlem 46029 dvsinax 46341 itgsubsticclem 46403 fargshiftf 47900

W3C validator