Theorem fmpt 7108

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 6677	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5939	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3126	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2849	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 485	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3160	. . . . . . 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 6541	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 595	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6730	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6238	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2811	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3445	. . 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 2739  ∀wral 3077  ∃wrex 3087  {crab 3413   ⊆ wss 3899   ↦ cmpt 5186  ^◡ccnv 5650  ran crn 5652   “ cima 5654   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 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  f1ompt  7109  fmpti  7110  fvmptelcdm  7111  fmptd  7112  fmptdf  7115  fompt  7116  rnmptss  7121  f1oresrab  7126  idref  7147  f1mpt  7263  f1stres  8023  f2ndres  8024  fmpox  8076  fmpoco  8104  onoviun  8344  onnseq  8345  mptelixpg  8956  dom2lem  9012  iinfi  9402  cantnfrescl  9670  acni2  10118  acnlem  10120  dfac4  10194  dfacacn  10213  fin23lem28  10411  axdc2lem  10519  axcclem  10528  ac6num  10550  uzf  12961  ccatalpha  14733  repsf  14917  rlim2  15656  rlimi  15673  o1fsum  15973  ackbijnn  15990  pcmptcl  17062  vdwlem11  17162  ismon2  17902  isepi2  17909  yonedalem3b  18446  smndex1gbasOLD  19092  efgsf  19936  gsummhm2  20146  gsummptcl  20174  gsummptfif1o  20175  gsummptfzcl  20176  gsumcom2  20182  gsummptnn0fz  20193  issrngd  21105  ipcl  21932  subrgasclcl  22369  evl1sca  22645  mavmulcl  22855  m2detleiblem3  22937  m2detleiblem4  22938  iinopn  23213  ordtrest2  23515  iscnp2  23550  discmp  23709  2ndcdisj  23768  ptunimpt  23907  pttopon  23908  ptcnplem  23933  upxp  23935  txdis1cn  23947  cnmpt11  23975  cnmpt21  23983  cnmptkp  23992  cnmptk1  23993  cnmpt1k  23994  cnmptkk  23995  cnmptk1p  23997  qtopeu  24028  uzrest  24209  txflf  24318  clsnsg  24422  tgpconncomp  24425  tsmsf1o  24457  prdsmet  24682  fsumcn  25184  cncfmpt1f  25228  iccpnfcnv  25258  lebnumlem1  25275  copco  25332  pcoass  25338  bcth3  25645  voliun  25868  i1f1lem  26003  iblcnlem  26102  limcvallem  26184  ellimc2  26190  cnmptlimc  26203  dvle  26320  dvfsumle  26334  dvfsumge  26335  dvfsumabs  26336  dvfsumlem2  26340  itgsubstlem  26361  sincn  26764  coscn  26765  rlimcxp  27294  harmonicbnd  27324  harmonicbnd2  27325  lgamgulmlem6  27354  sqff1o  27502  lgseisenlem3  27697  mptelee  29465  fmptdf2  33243  ordtrest2NEW  34548  ddemeas  34862  eulerpartgbij  34997  0rrv  35076  reprpmtf1o  35248  subfacf  35919  tailf  37143  fdc  38659  heiborlem5  38729  3factsumint  43055  dvle2  43102  fmpocos  43267  elrfirn2  43686  mptfcl  43710  mzpexpmpt  43735  mzpsubst  43738  rabdiophlem1  43787  rabdiophlem2  43788  pw2f1ocnv  44023  refsumcn  46016  fmptf  46220  fmptff  46250  fprodcnlem  46580  dvsinax  46892  itgsubsticclem  46954  fargshiftf  48491