Theorem fmpt 6874

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 6488	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5827	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3254	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2900	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 482	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3282	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 415	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4045	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 4015	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6359	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 585	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14	1	mptpreima 6092	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
15		fimacnv 6839	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
16	14, 15	syl5reqr 2871	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3381	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 220	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 211	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139  {crab 3142   ⊆ wss 3936   ↦ cmpt 5146  ^◡ccnv 5554  ran crn 5556   “ cima 5558   Fn wfn 6350  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  f1ompt  6875  fmpti  6876  fvmptelrn  6877  fmptd  6878  fmptdf  6881  rnmptss  6886  f1oresrab  6889  idref  6908  f1mpt  7019  f1stres  7713  f2ndres  7714  fmpox  7765  fmpoco  7790  onoviun  7980  onnseq  7981  mptelixpg  8499  dom2lem  8549  iinfi  8881  cantnfrescl  9139  acni2  9472  acnlem  9474  dfac4  9548  dfacacn  9567  fin23lem28  9762  axdc2lem  9870  axcclem  9879  ac6num  9901  uzf  12247  ccatalpha  13947  repsf  14135  rlim2  14853  rlimi  14870  o1fsum  15168  ackbijnn  15183  pcmptcl  16227  vdwlem11  16327  ismon2  17004  isepi2  17011  yonedalem3b  17529  smndex1gbas  18067  efgsf  18855  gsummhm2  19059  gsummptcl  19087  gsummptfif1o  19088  gsummptfzcl  19089  gsumcom2  19095  gsummptnn0fz  19106  issrngd  19632  subrgasclcl  20279  evl1sca  20497  ipcl  20777  mavmulcl  21156  m2detleiblem3  21238  m2detleiblem4  21239  iinopn  21510  ordtrest2  21812  iscnp2  21847  discmp  22006  2ndcdisj  22064  ptunimpt  22203  pttopon  22204  ptcnplem  22229  upxp  22231  txdis1cn  22243  cnmpt11  22271  cnmpt21  22279  cnmptkp  22288  cnmptk1  22289  cnmpt1k  22290  cnmptkk  22291  cnmptk1p  22293  qtopeu  22324  uzrest  22505  txflf  22614  clsnsg  22718  tgpconncomp  22721  tsmsf1o  22753  prdsmet  22980  fsumcn  23478  cncfmpt1f  23521  iccpnfcnv  23548  lebnumlem1  23565  copco  23622  pcoass  23628  bcth3  23934  voliun  24155  i1f1lem  24290  iblcnlem  24389  limcvallem  24469  ellimc2  24475  cnmptlimc  24488  dvle  24604  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem2  24624  itgsubstlem  24645  sincn  25032  coscn  25033  rlimcxp  25551  harmonicbnd  25581  harmonicbnd2  25582  lgamgulmlem6  25611  sqff1o  25759  lgseisenlem3  25953  fmptdF  30401  ordtrest2NEW  31166  ddemeas  31495  eulerpartgbij  31630  0rrv  31709  reprpmtf1o  31897  subfacf  32422  tailf  33723  fdc  35035  heiborlem5  35108  elrfirn2  39313  mptfcl  39337  mzpexpmpt  39362  mzpsubst  39365  rabdiophlem1  39418  rabdiophlem2  39419  pw2f1ocnv  39654  refsumcn  41307  fompt  41473  fmptf  41529  fprodcnlem  41900  dvsinax  42217  itgsubsticclem  42280  fargshiftf  43620  isomuspgrlem2b  44014