Theorem fmpt 7109

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 6679	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5949	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3130	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2853	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 485	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3164	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 18	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 418	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4022	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3976	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6544	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 595	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6732	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6241	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2815	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3451	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 221	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {cab 2743  ∀wral 3081  ∃wrex 3091  {crab 3418   ⊆ wss 3906   ↦ cmpt 5194  ^◡ccnv 5662  ran crn 5664   “ cima 5666   Fn wfn 6535  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  f1ompt  7110  fmpti  7111  fvmptelcdm  7112  fmptd  7113  fmptdf  7116  fompt  7117  rnmptss  7122  f1oresrab  7127  idref  7146  f1mpt  7261  f1stres  8012  f2ndres  8013  fmpox  8066  fmpoco  8092  onoviun  8332  onnseq  8333  mptelixpg  8935  dom2lem  8991  iinfi  9380  cantnfrescl  9648  acni2  10042  acnlem  10044  dfac4  10118  dfacacn  10137  fin23lem28  10335  axdc2lem  10443  axcclem  10452  ac6num  10474  uzf  12877  ccatalpha  14646  repsf  14830  rlim2  15567  rlimi  15584  o1fsum  15884  ackbijnn  15901  pcmptcl  16969  vdwlem11  17069  ismon2  17809  isepi2  17816  yonedalem3b  18353  smndex1gbasOLD  18986  efgsf  19823  gsummhm2  20033  gsummptcl  20061  gsummptfif1o  20062  gsummptfzcl  20063  gsumcom2  20069  gsummptnn0fz  20080  issrngd  20988  ipcl  21813  subrgasclcl  22248  evl1sca  22524  mavmulcl  22734  m2detleiblem3  22816  m2detleiblem4  22817  iinopn  23089  ordtrest2  23391  iscnp2  23426  discmp  23585  2ndcdisj  23644  ptunimpt  23783  pttopon  23784  ptcnplem  23809  upxp  23811  txdis1cn  23823  cnmpt11  23851  cnmpt21  23859  cnmptkp  23868  cnmptk1  23869  cnmpt1k  23870  cnmptkk  23871  cnmptk1p  23873  qtopeu  23904  uzrest  24085  txflf  24194  clsnsg  24298  tgpconncomp  24301  tsmsf1o  24333  prdsmet  24558  fsumcn  25060  cncfmpt1f  25104  iccpnfcnv  25134  lebnumlem1  25151  copco  25208  pcoass  25214  bcth3  25521  voliun  25744  i1f1lem  25879  iblcnlem  25979  limcvallem  26061  ellimc2  26067  cnmptlimc  26080  dvle  26197  dvfsumle  26211  dvfsumge  26212  dvfsumabs  26213  dvfsumlem2  26217  itgsubstlem  26238  sincn  26638  coscn  26639  rlimcxp  27169  harmonicbnd  27199  harmonicbnd2  27200  lgamgulmlem6  27229  sqff1o  27377  lgseisenlem3  27572  mptelee  29275  fmptdf2  33048  ordtrest2NEW  34353  ddemeas  34667  eulerpartgbij  34803  0rrv  34882  reprpmtf1o  35054  subfacf  35680  tailf  36919  fdc  38429  heiborlem5  38499  3factsumint  42825  dvle2  42872  fmpocos  43037  elrfirn2  43460  mptfcl  43484  mzpexpmpt  43509  mzpsubst  43512  rabdiophlem1  43561  rabdiophlem2  43562  pw2f1ocnv  43797  refsumcn  45783  fmptf  45987  fmptff  46017  fprodcnlem  46348  dvsinax  46660  itgsubsticclem  46722  fargshiftf  48222