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 6289

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 5933	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5292	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3054	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2676	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 503	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3011	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 449	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 3639	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	syl5eqss 3612	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 5808	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 695	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14	1	mptpreima 5545	. . . 4 ⊢ (^◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
15		fimacnv 6255	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (^◡𝐹 “ 𝐵) = 𝐴)
16	14, 15	syl5reqr 2659	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3096	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 207	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 198	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {cab 2596 ∀wral 2896 ∃wrex 2897 {crab 2900 ⊆ wss 3540 ↦ cmpt 4643 ^◡ccnv 5037 ran crn 5039 “ cima 5041 Fn wfn 5799 ⟶wf 5800

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812

This theorem is referenced by: f1ompt 6290 fmpti 6291 fmptd 6292 fmptdf 6294 rnmptss 6299 f1oresrab 6302 idref 6403 f1mpt 6419 f1stres 7081 f2ndres 7082 fmpt2x 7125 fmpt2co 7147 onoviun 7327 onnseq 7328 mptelixpg 7831 dom2lem 7881 iinfi 8206 cantnfrescl 8456 acni2 8752 acnlem 8754 dfac4 8828 dfacacn 8846 fin23lem28 9045 axdc2lem 9153 axcclem 9162 ac6num 9184 uzf 11566 ccatalpha 13228 repsf 13371 rlim2 14075 rlimi 14092 rlimmptrcl 14186 lo1mptrcl 14200 o1mptrcl 14201 o1fsum 14386 ackbijnn 14399 pcmptcl 15433 vdwlem11 15533 ismon2 16217 isepi2 16224 yonedalem3b 16742 efgsf 17965 gsummhm2 18162 gsummptcl 18189 gsummptfif1o 18190 gsummptfzcl 18191 gsumcom2 18197 gsummptnn0fz 18205 issrngd 18684 psrass1lem 19198 subrgasclcl 19320 evl1sca 19519 ipcl 19797 frlmgsum 19930 uvcresum 19951 mavmulcl 20172 m2detleiblem3 20254 m2detleiblem4 20255 iinopn 20532 ordtrest2 20818 iscnp2 20853 discmp 21011 2ndcdisj 21069 ptunimpt 21208 pttopon 21209 txcnp 21233 ptcnplem 21234 ptcnp 21235 upxp 21236 ptcn 21240 txdis1cn 21248 cnmpt11 21276 cnmpt1t 21278 cnmpt12 21280 cnmpt21 21284 cnmptkp 21293 cnmptk1 21294 cnmpt1k 21295 cnmptkk 21296 cnmptk1p 21298 cnmptk2 21299 qtopeu 21329 uzrest 21511 txflf 21620 cnmpt1plusg 21701 clsnsg 21723 tgpconcomp 21726 tsmsf1o 21758 cnmpt1vsca 21807 prdsmet 21985 cnmpt1ds 22453 fsumcn 22481 cncfmpt1f 22524 cncfmpt2ss 22526 iccpnfcnv 22551 lebnumlem1 22568 copco 22626 pcoass 22632 cnmpt1ip 22854 bcth3 22936 voliun 23129 mbfmptcl 23210 i1f1lem 23262 i1fposd 23280 iblcnlem 23361 itgss3 23387 limcvallem 23441 ellimc2 23447 cnmptlimc 23460 dvmptcl 23528 dvmptco 23541 dvle 23574 dvfsumle 23588 dvfsumge 23589 dvfsumabs 23590 dvmptrecl 23591 dvfsumlem2 23594 itgparts 23614 itgsubstlem 23615 itgsubst 23616 ulmss 23955 ulmdvlem2 23959 itgulm2 23967 sincn 24002 coscn 24003 logtayl 24206 rlimcxp 24500 harmonicbnd 24530 harmonicbnd2 24531 lgamgulmlem6 24560 sqff1o 24708 lgseisenlem3 24902 fargshiftf 26164 fmptdF 28836 ordtrest2NEW 29297 ddemeas 29626 eulerpartgbij 29761 0rrv 29840 subfacf 30411 tailf 31540 fdc 32711 heiborlem5 32784 elrfirn2 36277 mptfcl 36301 mzpexpmpt 36326 mzpsubst 36329 rabdiophlem1 36383 rabdiophlem2 36384 pw2f1ocnv 36622 refsumcn 38212 mptex2 38344 fompt 38374 fvmptelrn 38423 fprodcnlem 38666 dvsinax 38801 itgsubsticclem 38867

W3C validator