Theorem fmpt 6966

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 6557	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5853	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3183	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2826	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3210	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 3998	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3965	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6422	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 582	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6606	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6130	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2794	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3307	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 217	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {cab 2715  ∀wral 3063  ∃wrex 3064  {crab 3067   ⊆ wss 3883   ↦ cmpt 5153  ^◡ccnv 5579  ran crn 5581   “ cima 5583   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  f1ompt  6967  fmpti  6968  fvmptelrn  6969  fmptd  6970  fmptdf  6973  rnmptss  6978  f1oresrab  6981  idref  7000  f1mpt  7115  f1stres  7828  f2ndres  7829  fmpox  7880  fmpoco  7906  onoviun  8145  onnseq  8146  mptelixpg  8681  dom2lem  8735  iinfi  9106  cantnfrescl  9364  acni2  9733  acnlem  9735  dfac4  9809  dfacacn  9828  fin23lem28  10027  axdc2lem  10135  axcclem  10144  ac6num  10166  uzf  12514  ccatalpha  14226  repsf  14414  rlim2  15133  rlimi  15150  o1fsum  15453  ackbijnn  15468  pcmptcl  16520  vdwlem11  16620  ismon2  17363  isepi2  17370  yonedalem3b  17913  smndex1gbas  18456  efgsf  19250  gsummhm2  19455  gsummptcl  19483  gsummptfif1o  19484  gsummptfzcl  19485  gsumcom2  19491  gsummptnn0fz  19502  issrngd  20036  ipcl  20750  subrgasclcl  21185  evl1sca  21410  mavmulcl  21604  m2detleiblem3  21686  m2detleiblem4  21687  iinopn  21959  ordtrest2  22263  iscnp2  22298  discmp  22457  2ndcdisj  22515  ptunimpt  22654  pttopon  22655  ptcnplem  22680  upxp  22682  txdis1cn  22694  cnmpt11  22722  cnmpt21  22730  cnmptkp  22739  cnmptk1  22740  cnmpt1k  22741  cnmptkk  22742  cnmptk1p  22744  qtopeu  22775  uzrest  22956  txflf  23065  clsnsg  23169  tgpconncomp  23172  tsmsf1o  23204  prdsmet  23431  fsumcn  23939  cncfmpt1f  23983  iccpnfcnv  24013  lebnumlem1  24030  copco  24087  pcoass  24093  bcth3  24400  voliun  24623  i1f1lem  24758  iblcnlem  24858  limcvallem  24940  ellimc2  24946  cnmptlimc  24959  dvle  25076  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvfsumlem2  25096  itgsubstlem  25117  sincn  25508  coscn  25509  rlimcxp  26028  harmonicbnd  26058  harmonicbnd2  26059  lgamgulmlem6  26088  sqff1o  26236  lgseisenlem3  26430  fmptdF  30895  ordtrest2NEW  31775  ddemeas  32104  eulerpartgbij  32239  0rrv  32318  reprpmtf1o  32506  subfacf  33037  tailf  34491  fdc  35830  heiborlem5  35900  3factsumint  39961  dvle2  40008  elrfirn2  40434  mptfcl  40458  mzpexpmpt  40483  mzpsubst  40486  rabdiophlem1  40539  rabdiophlem2  40540  pw2f1ocnv  40775  refsumcn  42462  fompt  42619  fmptf  42672  fprodcnlem  43030  dvsinax  43344  itgsubsticclem  43406  fargshiftf  44780  isomuspgrlem2b  45169