Theorem fmpt 7103

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 6673	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5945	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3134	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2857	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 484	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3168	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 18	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 417	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4029	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3983	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6538	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 594	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6726	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6237	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2819	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3456	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 221	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {cab 2747  ∀wral 3085  ∃wrex 3095  {crab 3423   ⊆ wss 3913   ↦ cmpt 5193  ^◡ccnv 5658  ran crn 5660   “ cima 5662   Fn wfn 6529  ⟶wf 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6536  df-fn 6537  df-f 6538

This theorem is referenced by:  f1ompt  7104  fmpti  7105  fvmptelcdm  7106  fmptd  7107  fmptdf  7110  fompt  7111  rnmptss  7116  f1oresrab  7121  idref  7140  f1mpt  7257  f1stres  8006  f2ndres  8007  fmpox  8060  fmpoco  8086  onoviun  8326  onnseq  8327  mptelixpg  8929  dom2lem  8985  iinfi  9373  cantnfrescl  9641  acni2  10026  acnlem  10028  dfac4  10102  dfacacn  10121  fin23lem28  10320  axdc2lem  10428  axcclem  10437  ac6num  10459  uzf  12861  ccatalpha  14627  repsf  14806  rlim2  15543  rlimi  15560  o1fsum  15861  ackbijnn  15878  pcmptcl  16947  vdwlem11  17047  ismon2  17787  isepi2  17794  yonedalem3b  18331  smndex1gbasOLD  18958  efgsf  19795  gsummhm2  20005  gsummptcl  20033  gsummptfif1o  20034  gsummptfzcl  20035  gsumcom2  20041  gsummptnn0fz  20052  issrngd  20932  ipcl  21748  subrgasclcl  22183  evl1sca  22459  mavmulcl  22669  m2detleiblem3  22751  m2detleiblem4  22752  iinopn  23024  ordtrest2  23326  iscnp2  23361  discmp  23520  2ndcdisj  23578  ptunimpt  23717  pttopon  23718  ptcnplem  23743  upxp  23745  txdis1cn  23757  cnmpt11  23785  cnmpt21  23793  cnmptkp  23802  cnmptk1  23803  cnmpt1k  23804  cnmptkk  23805  cnmptk1p  23807  qtopeu  23838  uzrest  24019  txflf  24128  clsnsg  24232  tgpconncomp  24235  tsmsf1o  24267  prdsmet  24492  fsumcn  24994  cncfmpt1f  25038  iccpnfcnv  25068  lebnumlem1  25085  copco  25142  pcoass  25148  bcth3  25455  voliun  25678  i1f1lem  25813  iblcnlem  25913  limcvallem  25995  ellimc2  26001  cnmptlimc  26014  dvle  26131  dvfsumle  26145  dvfsumge  26146  dvfsumabs  26147  dvfsumlem2  26151  itgsubstlem  26172  sincn  26569  coscn  26570  rlimcxp  27100  harmonicbnd  27130  harmonicbnd2  27131  lgamgulmlem6  27160  sqff1o  27308  lgseisenlem3  27503  mptelee  29181  fmptdF  32938  ordtrest2NEW  34254  ddemeas  34567  eulerpartgbij  34703  0rrv  34782  reprpmtf1o  34954  subfacf  35562  tailf  36771  fdc  38279  heiborlem5  38349  3factsumint  42677  dvle2  42724  fmpocos  42889  elrfirn2  43314  mptfcl  43338  mzpexpmpt  43363  mzpsubst  43366  rabdiophlem1  43415  rabdiophlem2  43416  pw2f1ocnv  43651  refsumcn  45637  fmptf  45841  fmptff  45871  fprodcnlem  46202  dvsinax  46514  itgsubsticclem  46576  fargshiftf  48073