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 6672	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5941	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3125	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2848	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 485	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3159	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 18	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 418	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4015	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3969	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6537	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 595	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6725	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6234	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2810	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3444	. . 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 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  {crab 3412   ⊆ wss 3899   ↦ cmpt 5186  ^◡ccnv 5654  ran crn 5656   “ cima 5658   Fn wfn 6528  ⟶wf 6529

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537

This theorem is used by:  f1ompt  7104  fmpti  7105  fvmptelcdm  7106  fmptd  7107  fmptdf  7110  fompt  7111  rnmptss  7116  f1oresrab  7121  idref  7142  f1mpt  7258  f1stres  8010  f2ndres  8011  fmpox  8064  fmpoco  8092  onoviun  8332  onnseq  8333  mptelixpg  8942  dom2lem  8998  iinfi  9387  cantnfrescl  9655  acni2  10049  acnlem  10051  dfac4  10125  dfacacn  10144  fin23lem28  10342  axdc2lem  10450  axcclem  10459  ac6num  10481  uzf  12890  ccatalpha  14660  repsf  14844  rlim2  15583  rlimi  15600  o1fsum  15900  ackbijnn  15917  pcmptcl  16983  vdwlem11  17083  ismon2  17823  isepi2  17830  yonedalem3b  18367  smndex1gbasOLD  19012  efgsf  19856  gsummhm2  20066  gsummptcl  20094  gsummptfif1o  20095  gsummptfzcl  20096  gsumcom2  20102  gsummptnn0fz  20113  issrngd  21021  ipcl  21846  subrgasclcl  22283  evl1sca  22559  mavmulcl  22769  m2detleiblem3  22851  m2detleiblem4  22852  iinopn  23127  ordtrest2  23429  iscnp2  23464  discmp  23623  2ndcdisj  23682  ptunimpt  23821  pttopon  23822  ptcnplem  23847  upxp  23849  txdis1cn  23861  cnmpt11  23889  cnmpt21  23897  cnmptkp  23906  cnmptk1  23907  cnmpt1k  23908  cnmptkk  23909  cnmptk1p  23911  qtopeu  23942  uzrest  24123  txflf  24232  clsnsg  24336  tgpconncomp  24339  tsmsf1o  24371  prdsmet  24596  fsumcn  25098  cncfmpt1f  25142  iccpnfcnv  25172  lebnumlem1  25189  copco  25246  pcoass  25252  bcth3  25559  voliun  25782  i1f1lem  25917  iblcnlem  26016  limcvallem  26098  ellimc2  26104  cnmptlimc  26117  dvle  26234  dvfsumle  26248  dvfsumge  26249  dvfsumabs  26250  dvfsumlem2  26254  itgsubstlem  26275  sincn  26680  coscn  26681  rlimcxp  27210  harmonicbnd  27240  harmonicbnd2  27241  lgamgulmlem6  27270  sqff1o  27418  lgseisenlem3  27613  mptelee  29351  fmptdf2  33129  ordtrest2NEW  34433  ddemeas  34747  eulerpartgbij  34883  0rrv  34962  reprpmtf1o  35134  subfacf  35754  tailf  36994  fdc  38495  heiborlem5  38565  3factsumint  42891  dvle2  42938  fmpocos  43103  elrfirn2  43541  mptfcl  43565  mzpexpmpt  43590  mzpsubst  43593  rabdiophlem1  43642  rabdiophlem2  43643  pw2f1ocnv  43878  refsumcn  45864  fmptf  46068  fmptff  46098  fprodcnlem  46429  dvsinax  46741  itgsubsticclem  46803  fargshiftf  48340