Theorem mptpreima 6252

Description: The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)

Hypothesis

Ref	Expression
dmmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
mptpreima	⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem mptpreima

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmmpt.1	. . . . . 6 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2		df-mpt 5190	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
3	1, 2	eqtri 2786	. . . . 5 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	3	cnveqi 5859	. . . 4 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5		cnvopab 6143	. . . 4 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	4, 5	eqtri 2786	. . 3 ⊢ ◡𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
7	6	imaeq1i 6061	. 2 ⊢ (◡𝐹 “ 𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶)
8		df-ima 5668	. . 3 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶)
9		resopab 6038	. . . . 5 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
10	9	rneqi 5926	. . . 4 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
11		ancom 466	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶))
12		anass 474	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
13	11, 12	bitri 278	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
14	13	exbii 1881	. . . . . . 7 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
15		19.42v 1988	. . . . . . . 8 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
16		dfclel 2840	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶))
17	16	bicomi 227	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ 𝐵 ∈ 𝐶)
18	17	anbi2i 635	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
19	15, 18	bitri 278	. . . . . . 7 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
20	14, 19	bitri 278	. . . . . 6 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
21	20	abbii 2830	. . . . 5 ⊢ {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
22		rnopab 5943	. . . . 5 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
23		df-rab 3417	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
24	21, 22, 23	3eqtr4i 2796	. . . 4 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
25	10, 24	eqtri 2786	. . 3 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
26	8, 25	eqtri 2786	. 2 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
27	7, 26	eqtri 2786	1 ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  {cab 2741  {crab 3416  {copab 5170   ↦ cmpt 5189  ^◡ccnv 5654  ran crn 5656   ↾ cres 5657   “ cima 5658

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 5252  ax-pr 5395

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-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  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 4839  df-br 5107  df-opab 5171  df-mpt 5190  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  mptiniseg  6253  dmmpt  6254  fmpt  7134  f1oresrab  7152  mptsuppdifd  8231  r0weon  10118  compss  10481  infrenegsup  12327  eqglact  19420  odngen  19821  pjdm  22043  psrbagsn  22402  coe1mul2lem2  22617  xkoccn  23968  txcnmpt  23973  txdis1cn  23984  pthaus  23987  txkgen  24001  xkoco1cn  24006  xkoco2cn  24007  xkoinjcn  24036  txconn  24038  imasnopn  24039  imasncld  24040  imasncls  24041  ptcmplem1  24401  ptcmplem3  24403  ptcmplem4  24404  tmdgsum2  24445  symgtgp  24455  tgpconncompeqg  24461  ghmcnp  24464  tgpt0  24468  qustgpopn  24469  qustgphaus  24472  eltsms  24482  prdsxmslem2  24878  efopn  27016  atansopn  27290  xrlimcnp  27326  fpwrelmapffslem  33394  ptrest  38729  mbfposadd  38777  cnambfre  38778  itg2addnclem2  38782  iblabsnclem  38793  ftc1anclem1  38803  ftc1anclem6  38808  resuppsinopn  43607  pwfi2f1o  44291  smfpimioo  48002  dvsec  51136  dvcsc  51137  dvcot  51138