Theorem fmpt 7107

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 6676	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5945	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3127	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2850	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 485	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3161	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 18	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 418	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4018	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3972	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6541	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 595	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6729	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6238	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2812	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3447	. . 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 2740  ∀wral 3078  ∃wrex 3088  {crab 3414   ⊆ wss 3902   ↦ cmpt 5190  ^◡ccnv 5658  ran crn 5660   “ cima 5662   Fn wfn 6532  ⟶wf 6533

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 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  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 6539  df-fn 6540  df-f 6541

This theorem is used by:  f1ompt  7108  fmpti  7109  fvmptelcdm  7110  fmptd  7111  fmptdf  7114  fompt  7115  rnmptss  7120  f1oresrab  7125  idref  7146  f1mpt  7262  f1stres  8014  f2ndres  8015  fmpox  8068  fmpoco  8096  onoviun  8336  onnseq  8337  mptelixpg  8946  dom2lem  9002  iinfi  9391  cantnfrescl  9659  acni2  10053  acnlem  10055  dfac4  10129  dfacacn  10148  fin23lem28  10346  axdc2lem  10454  axcclem  10463  ac6num  10485  uzf  12894  ccatalpha  14664  repsf  14848  rlim2  15587  rlimi  15604  o1fsum  15904  ackbijnn  15921  pcmptcl  16989  vdwlem11  17089  ismon2  17829  isepi2  17836  yonedalem3b  18373  smndex1gbasOLD  19018  efgsf  19862  gsummhm2  20072  gsummptcl  20100  gsummptfif1o  20101  gsummptfzcl  20102  gsumcom2  20108  gsummptnn0fz  20119  issrngd  21027  ipcl  21852  subrgasclcl  22289  evl1sca  22565  mavmulcl  22775  m2detleiblem3  22857  m2detleiblem4  22858  iinopn  23133  ordtrest2  23435  iscnp2  23470  discmp  23629  2ndcdisj  23688  ptunimpt  23827  pttopon  23828  ptcnplem  23853  upxp  23855  txdis1cn  23867  cnmpt11  23895  cnmpt21  23903  cnmptkp  23912  cnmptk1  23913  cnmpt1k  23914  cnmptkk  23915  cnmptk1p  23917  qtopeu  23948  uzrest  24129  txflf  24238  clsnsg  24342  tgpconncomp  24345  tsmsf1o  24377  prdsmet  24602  fsumcn  25104  cncfmpt1f  25148  iccpnfcnv  25178  lebnumlem1  25195  copco  25252  pcoass  25258  bcth3  25565  voliun  25788  i1f1lem  25923  iblcnlem  26023  limcvallem  26105  ellimc2  26111  cnmptlimc  26124  dvle  26241  dvfsumle  26255  dvfsumge  26256  dvfsumabs  26257  dvfsumlem2  26261  itgsubstlem  26282  sincn  26687  coscn  26688  rlimcxp  27218  harmonicbnd  27248  harmonicbnd2  27249  lgamgulmlem6  27278  sqff1o  27426  lgseisenlem3  27621  mptelee  29359  fmptdf2  33137  ordtrest2NEW  34441  ddemeas  34755  eulerpartgbij  34891  0rrv  34970  reprpmtf1o  35142  subfacf  35762  tailf  37002  fdc  38503  heiborlem5  38573  3factsumint  42899  dvle2  42946  fmpocos  43111  elrfirn2  43549  mptfcl  43573  mzpexpmpt  43598  mzpsubst  43601  rabdiophlem1  43650  rabdiophlem2  43651  pw2f1ocnv  43886  refsumcn  45872  fmptf  46076  fmptff  46106  fprodcnlem  46437  dvsinax  46749  itgsubsticclem  46811  fargshiftf  48348