Theorem fmpt 6993

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 6582	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5867	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3185	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2827	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 480	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3212	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 17	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 413	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4003	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3970	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6441	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 583	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6631	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6146	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2794	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3315	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 217	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 208	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {cab 2716  ∀wral 3065  ∃wrex 3066  {crab 3069   ⊆ wss 3888   ↦ cmpt 5158  ^◡ccnv 5589  ran crn 5591   “ cima 5593   Fn wfn 6432  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  f1ompt  6994  fmpti  6995  fvmptelrn  6996  fmptd  6997  fmptdf  7000  rnmptss  7005  f1oresrab  7008  idref  7027  f1mpt  7143  f1stres  7864  f2ndres  7865  fmpox  7916  fmpoco  7944  onoviun  8183  onnseq  8184  mptelixpg  8732  dom2lem  8789  iinfi  9185  cantnfrescl  9443  acni2  9811  acnlem  9813  dfac4  9887  dfacacn  9906  fin23lem28  10105  axdc2lem  10213  axcclem  10222  ac6num  10244  uzf  12594  ccatalpha  14307  repsf  14495  rlim2  15214  rlimi  15231  o1fsum  15534  ackbijnn  15549  pcmptcl  16601  vdwlem11  16701  ismon2  17455  isepi2  17462  yonedalem3b  18006  smndex1gbas  18550  efgsf  19344  gsummhm2  19549  gsummptcl  19577  gsummptfif1o  19578  gsummptfzcl  19579  gsumcom2  19585  gsummptnn0fz  19596  issrngd  20130  ipcl  20847  subrgasclcl  21284  evl1sca  21509  mavmulcl  21705  m2detleiblem3  21787  m2detleiblem4  21788  iinopn  22060  ordtrest2  22364  iscnp2  22399  discmp  22558  2ndcdisj  22616  ptunimpt  22755  pttopon  22756  ptcnplem  22781  upxp  22783  txdis1cn  22795  cnmpt11  22823  cnmpt21  22831  cnmptkp  22840  cnmptk1  22841  cnmpt1k  22842  cnmptkk  22843  cnmptk1p  22845  qtopeu  22876  uzrest  23057  txflf  23166  clsnsg  23270  tgpconncomp  23273  tsmsf1o  23305  prdsmet  23532  fsumcn  24042  cncfmpt1f  24086  iccpnfcnv  24116  lebnumlem1  24133  copco  24190  pcoass  24196  bcth3  24504  voliun  24727  i1f1lem  24862  iblcnlem  24962  limcvallem  25044  ellimc2  25050  cnmptlimc  25063  dvle  25180  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvfsumlem2  25200  itgsubstlem  25221  sincn  25612  coscn  25613  rlimcxp  26132  harmonicbnd  26162  harmonicbnd2  26163  lgamgulmlem6  26192  sqff1o  26340  lgseisenlem3  26534  fmptdF  31002  ordtrest2NEW  31882  ddemeas  32213  eulerpartgbij  32348  0rrv  32427  reprpmtf1o  32615  subfacf  33146  tailf  34573  fdc  35912  heiborlem5  35982  3factsumint  40040  dvle2  40087  elrfirn2  40525  mptfcl  40549  mzpexpmpt  40574  mzpsubst  40577  rabdiophlem1  40630  rabdiophlem2  40631  pw2f1ocnv  40866  refsumcn  42580  fompt  42737  fmptf  42790  fprodcnlem  43147  dvsinax  43461  itgsubsticclem  43523  fargshiftf  44903  isomuspgrlem2b  45292