Theorem fmpt 7056

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 6632	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5906	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3101	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2825	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 479	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3135	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 412	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4008	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3961	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 584	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6684	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6196	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2787	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3423	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 218	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  {crab 3390   ⊆ wss 3890   ↦ cmpt 5167  ^◡ccnv 5623  ran crn 5625   “ cima 5627   Fn wfn 6487  ⟶wf 6488

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  f1ompt  7057  fmpti  7058  fvmptelcdm  7059  fmptd  7060  fmptdf  7063  fompt  7064  rnmptss  7069  f1oresrab  7074  idref  7093  f1mpt  7209  f1stres  7959  f2ndres  7960  fmpox  8013  fmpoco  8038  onoviun  8276  onnseq  8277  mptelixpg  8876  dom2lem  8932  iinfi  9323  cantnfrescl  9588  acni2  9959  acnlem  9961  dfac4  10035  dfacacn  10055  fin23lem28  10253  axdc2lem  10361  axcclem  10370  ac6num  10392  uzf  12782  ccatalpha  14547  repsf  14726  rlim2  15449  rlimi  15466  o1fsum  15767  ackbijnn  15784  pcmptcl  16853  vdwlem11  16953  ismon2  17692  isepi2  17699  yonedalem3b  18236  smndex1gbasOLD  18862  efgsf  19695  gsummhm2  19905  gsummptcl  19933  gsummptfif1o  19934  gsummptfzcl  19935  gsumcom2  19941  gsummptnn0fz  19952  issrngd  20823  ipcl  21623  subrgasclcl  22055  evl1sca  22309  mavmulcl  22522  m2detleiblem3  22604  m2detleiblem4  22605  iinopn  22877  ordtrest2  23179  iscnp2  23214  discmp  23373  2ndcdisj  23431  ptunimpt  23570  pttopon  23571  ptcnplem  23596  upxp  23598  txdis1cn  23610  cnmpt11  23638  cnmpt21  23646  cnmptkp  23655  cnmptk1  23656  cnmpt1k  23657  cnmptkk  23658  cnmptk1p  23660  qtopeu  23691  uzrest  23872  txflf  23981  clsnsg  24085  tgpconncomp  24088  tsmsf1o  24120  prdsmet  24345  fsumcn  24847  cncfmpt1f  24891  iccpnfcnv  24921  lebnumlem1  24938  copco  24995  pcoass  25001  bcth3  25308  voliun  25531  i1f1lem  25666  iblcnlem  25766  limcvallem  25848  ellimc2  25854  cnmptlimc  25867  dvle  25984  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  dvfsumlem2  26004  itgsubstlem  26025  sincn  26422  coscn  26423  rlimcxp  26951  harmonicbnd  26981  harmonicbnd2  26982  lgamgulmlem6  27011  sqff1o  27159  lgseisenlem3  27354  mptelee  28977  fmptdF  32744  ordtrest2NEW  34083  ddemeas  34396  eulerpartgbij  34532  0rrv  34611  reprpmtf1o  34786  subfacf  35373  tailf  36573  fdc  38080  heiborlem5  38150  3factsumint  42478  dvle2  42525  fmpocos  42689  elrfirn2  43142  mptfcl  43166  mzpexpmpt  43191  mzpsubst  43194  rabdiophlem1  43247  rabdiophlem2  43248  pw2f1ocnv  43483  refsumcn  45479  fmptf  45686  fmptff  45716  fprodcnlem  46047  dvsinax  46359  itgsubsticclem  46421  fargshiftf  47912