Theorem fmpt 7058

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 6641	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5910	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3117	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2825	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 480	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3148	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 413	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4025	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3992	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6500	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6690	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6190	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2791	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3436	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 217	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2713  ∀wral 3064  ∃wrex 3073  {crab 3407   ⊆ wss 3910   ↦ cmpt 5188  ^◡ccnv 5632  ran crn 5634   “ cima 5636   Fn wfn 6491  ⟶wf 6492

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-fun 6498  df-fn 6499  df-f 6500

This theorem is referenced by:  f1ompt  7059  fmpti  7060  fvmptelcdm  7061  fmptd  7062  fmptdf  7065  rnmptss  7070  f1oresrab  7073  idref  7092  f1mpt  7208  f1stres  7945  f2ndres  7946  fmpox  7999  fmpoco  8027  onoviun  8289  onnseq  8290  mptelixpg  8873  dom2lem  8932  iinfi  9353  cantnfrescl  9612  acni2  9982  acnlem  9984  dfac4  10058  dfacacn  10077  fin23lem28  10276  axdc2lem  10384  axcclem  10393  ac6num  10415  uzf  12766  ccatalpha  14481  repsf  14661  rlim2  15378  rlimi  15395  o1fsum  15698  ackbijnn  15713  pcmptcl  16763  vdwlem11  16863  ismon2  17617  isepi2  17624  yonedalem3b  18168  smndex1gbas  18712  efgsf  19511  gsummhm2  19716  gsummptcl  19744  gsummptfif1o  19745  gsummptfzcl  19746  gsumcom2  19752  gsummptnn0fz  19763  issrngd  20320  ipcl  21037  subrgasclcl  21475  evl1sca  21700  mavmulcl  21896  m2detleiblem3  21978  m2detleiblem4  21979  iinopn  22251  ordtrest2  22555  iscnp2  22590  discmp  22749  2ndcdisj  22807  ptunimpt  22946  pttopon  22947  ptcnplem  22972  upxp  22974  txdis1cn  22986  cnmpt11  23014  cnmpt21  23022  cnmptkp  23031  cnmptk1  23032  cnmpt1k  23033  cnmptkk  23034  cnmptk1p  23036  qtopeu  23067  uzrest  23248  txflf  23357  clsnsg  23461  tgpconncomp  23464  tsmsf1o  23496  prdsmet  23723  fsumcn  24233  cncfmpt1f  24277  iccpnfcnv  24307  lebnumlem1  24324  copco  24381  pcoass  24387  bcth3  24695  voliun  24918  i1f1lem  25053  iblcnlem  25153  limcvallem  25235  ellimc2  25241  cnmptlimc  25254  dvle  25371  dvfsumle  25385  dvfsumge  25386  dvfsumabs  25387  dvfsumlem2  25391  itgsubstlem  25412  sincn  25803  coscn  25804  rlimcxp  26323  harmonicbnd  26353  harmonicbnd2  26354  lgamgulmlem6  26383  sqff1o  26531  lgseisenlem3  26725  fmptdF  31572  ordtrest2NEW  32504  ddemeas  32835  eulerpartgbij  32972  0rrv  33051  reprpmtf1o  33239  subfacf  33769  tailf  34847  fdc  36204  heiborlem5  36274  3factsumint  40482  dvle2  40529  elrfirn2  41005  mptfcl  41029  mzpexpmpt  41054  mzpsubst  41057  rabdiophlem1  41110  rabdiophlem2  41111  pw2f1ocnv  41347  refsumcn  43225  fompt  43401  fmptf  43455  fmptff  43488  fprodcnlem  43830  dvsinax  44144  itgsubsticclem  44206  fargshiftf  45622  isomuspgrlem2b  46011