Theorem fmpt 7142

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 6709	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5951	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3129	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2852	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 485	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3163	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 18	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 418	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 3995	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3951	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6570	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 595	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6762	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6258	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2813	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3448	. . 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 2147  {cab 2741  ∀wral 3080  ∃wrex 3090  {crab 3416   ⊆ wss 3900   ↦ cmpt 5192  ^◡ccnv 5657  ran crn 5659   “ cima 5661   Fn wfn 6561  ⟶wf 6562

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  f1ompt  7143  fmpti  7144  fvmptelcdm  7145  fmptd  7146  fmptdf  7149  fompt  7150  rnmptss  7155  f1oresrab  7160  idref  7181  f1mpt  7296  f1stres  8059  f2ndres  8060  fmpox  8113  fmpoco  8142  onoviun  8389  onnseq  8390  mptelixpg  9001  dom2lem  9057  iinfi  9446  cantnfrescl  9714  acni2  10164  acnlem  10166  dfac4  10240  dfacacn  10259  fin23lem28  10457  axdc2lem  10565  axcclem  10574  ac6num  10596  uzf  13008  ccatalpha  14781  repsf  14966  rlim2  15707  rlimi  15724  o1fsum  16024  ackbijnn  16041  pcmptcl  17113  vdwlem11  17213  ismon2  17959  isepi2  17966  yonedalem3b  18503  smndex1gbasOLD  19149  efgsf  19994  gsummhm2  20204  gsummptcl  20232  gsummptfif1o  20233  gsummptfzcl  20234  gsumcom2  20240  gsummptnn0fz  20251  issrngd  21163  ipcl  21994  subrgasclcl  22431  evl1sca  22707  mavmulcl  22917  m2detleiblem3  22999  m2detleiblem4  23000  iinopn  23275  ordtrest2  23577  iscnp2  23612  discmp  23771  2ndcdisj  23830  ptunimpt  23969  pttopon  23970  ptcnplem  23995  upxp  23997  txdis1cn  24009  cnmpt11  24037  cnmpt21  24045  cnmptkp  24054  cnmptk1  24055  cnmpt1k  24056  cnmptkk  24057  cnmptk1p  24059  qtopeu  24090  uzrest  24271  txflf  24380  clsnsg  24484  tgpconncomp  24487  tsmsf1o  24519  prdsmet  24744  fsumcn  25246  cncfmpt1f  25290  iccpnfcnv  25320  lebnumlem1  25337  copco  25394  pcoass  25400  bcth3  25707  voliun  25930  i1f1lem  26065  iblcnlem  26164  limcvallem  26246  ellimc2  26252  cnmptlimc  26265  dvle  26382  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  dvfsumlem2  26402  itgsubstlem  26423  sincn  26828  coscn  26829  rlimcxp  27358  harmonicbnd  27388  harmonicbnd2  27389  lgamgulmlem6  27418  sqff1o  27566  lgseisenlem3  27761  mptelee  29529  fmptdf2  33348  ordtrest2NEW  34666  ddemeas  34980  eulerpartgbij  35115  0rrv  35194  reprpmtf1o  35366  subfacf  36148  tailf  37378  fdc  38945  heiborlem5  39015  3factsumint  43341  dvle2  43388  fmpocos  43554  elrfirn2  43973  mptfcl  43997  mzpexpmpt  44022  mzpsubst  44025  rabdiophlem1  44074  rabdiophlem2  44075  pw2f1ocnv  44310  refsumcn  46321  fmptf  46524  fmptff  46554  fprodcnlem  46884  dvsinax  47196  itgsubsticclem  47258  fargshiftf  48795