Theorem fmpt 7105

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 6675	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹 Fn 𝐴)
3	1	rnmpt 5947	. . . 4 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶}
4		r19.29 3128	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → ∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶))
5		eleq1 2851	. . . . . . . . 9 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵))
6	5	biimparc 484	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
7	6	rexlimivw 3162	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
8	4, 7	syl 18	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶) → 𝑦 ∈ 𝐵)
9	8	ex 417	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐶 → 𝑦 ∈ 𝐵))
10	9	abssdv 4021	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐶} ⊆ 𝐵)
11	3, 10	eqsstrid 3975	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → ran 𝐹 ⊆ 𝐵)
12		df-f 6540	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
13	2, 11, 12	sylanbrc 594	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → 𝐹:𝐴⟶𝐵)
14		fimacnv 6728	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴)
15	1	mptpreima 6239	. . . 4 ⊢ (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵}
16	14, 15	eqtr3di 2813	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵})
17		rabid2 3449	. . 3 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ 𝐵} ↔ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
18	16, 17	sylib 221	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵)
19	13, 18	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {cab 2741  ∀wral 3079  ∃wrex 3089  {crab 3416   ⊆ wss 3905   ↦ cmpt 5192  ^◡ccnv 5660  ran crn 5662   “ cima 5664   Fn wfn 6531  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  f1ompt  7106  fmpti  7107  fvmptelcdm  7108  fmptd  7109  fmptdf  7112  fompt  7113  rnmptss  7118  f1oresrab  7123  idref  7142  f1mpt  7259  f1stres  8006  f2ndres  8007  fmpox  8060  fmpoco  8086  onoviun  8326  onnseq  8327  mptelixpg  8929  dom2lem  8985  iinfi  9373  cantnfrescl  9641  acni2  10026  acnlem  10028  dfac4  10102  dfacacn  10121  fin23lem28  10319  axdc2lem  10427  axcclem  10436  ac6num  10458  uzf  12860  ccatalpha  14627  repsf  14806  rlim2  15543  rlimi  15560  o1fsum  15861  ackbijnn  15878  pcmptcl  16946  vdwlem11  17046  ismon2  17786  isepi2  17793  yonedalem3b  18330  smndex1gbasOLD  18957  efgsf  19794  gsummhm2  20004  gsummptcl  20032  gsummptfif1o  20033  gsummptfzcl  20034  gsumcom2  20040  gsummptnn0fz  20051  issrngd  20958  ipcl  21783  subrgasclcl  22218  evl1sca  22494  mavmulcl  22704  m2detleiblem3  22786  m2detleiblem4  22787  iinopn  23059  ordtrest2  23361  iscnp2  23396  discmp  23555  2ndcdisj  23613  ptunimpt  23752  pttopon  23753  ptcnplem  23778  upxp  23780  txdis1cn  23792  cnmpt11  23820  cnmpt21  23828  cnmptkp  23837  cnmptk1  23838  cnmpt1k  23839  cnmptkk  23840  cnmptk1p  23842  qtopeu  23873  uzrest  24054  txflf  24163  clsnsg  24267  tgpconncomp  24270  tsmsf1o  24302  prdsmet  24527  fsumcn  25029  cncfmpt1f  25073  iccpnfcnv  25103  lebnumlem1  25120  copco  25177  pcoass  25183  bcth3  25490  voliun  25713  i1f1lem  25848  iblcnlem  25948  limcvallem  26030  ellimc2  26036  cnmptlimc  26049  dvle  26166  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  dvfsumlem2  26186  itgsubstlem  26207  sincn  26607  coscn  26608  rlimcxp  27138  harmonicbnd  27168  harmonicbnd2  27169  lgamgulmlem6  27198  sqff1o  27346  lgseisenlem3  27541  mptelee  29244  fmptdF  33001  ordtrest2NEW  34313  ddemeas  34626  eulerpartgbij  34762  0rrv  34841  reprpmtf1o  35013  subfacf  35667  tailf  36886  fdc  38396  heiborlem5  38466  3factsumint  42792  dvle2  42839  fmpocos  43004  elrfirn2  43427  mptfcl  43451  mzpexpmpt  43476  mzpsubst  43479  rabdiophlem1  43528  rabdiophlem2  43529  pw2f1ocnv  43764  refsumcn  45750  fmptf  45954  fmptff  45984  fprodcnlem  46315  dvsinax  46627  itgsubsticclem  46689  fargshiftf  48189