Theorem mptpreima 6130

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 5154	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
3	1, 2	eqtri 2766	. . . . 5 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	3	cnveqi 5772	. . . 4 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5		cnvopab 6031	. . . 4 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	4, 5	eqtri 2766	. . 3 ⊢ ◡𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
7	6	imaeq1i 5955	. 2 ⊢ (◡𝐹 “ 𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶)
8		df-ima 5593	. . 3 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶)
9		resopab 5931	. . . . 5 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
10	9	rneqi 5835	. . . 4 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
11		ancom 460	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶))
12		anass 468	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
13	11, 12	bitri 274	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
14	13	exbii 1851	. . . . . . 7 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
15		19.42v 1958	. . . . . . . 8 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
16		dfclel 2818	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶))
17	16	bicomi 223	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ 𝐵 ∈ 𝐶)
18	17	anbi2i 622	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
19	15, 18	bitri 274	. . . . . . 7 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
20	14, 19	bitri 274	. . . . . 6 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
21	20	abbii 2809	. . . . 5 ⊢ {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
22		rnopab 5852	. . . . 5 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
23		df-rab 3072	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
24	21, 22, 23	3eqtr4i 2776	. . . 4 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
25	10, 24	eqtri 2766	. . 3 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
26	8, 25	eqtri 2766	. 2 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
27	7, 26	eqtri 2766	1 ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  {crab 3067  {copab 5132   ↦ cmpt 5153  ^◡ccnv 5579  ran crn 5581   ↾ cres 5582   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-xp 5586  df-rel 5587  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  mptiniseg  6131  dmmpt  6132  fmpt  6966  f1oresrab  6981  mptsuppdifd  7973  r0weon  9699  compss  10063  infrenegsup  11888  eqglact  18722  odngen  19097  pjdm  20824  psrbagsn  21181  coe1mul2lem2  21349  xkoccn  22678  txcnmpt  22683  txdis1cn  22694  pthaus  22697  txkgen  22711  xkoco1cn  22716  xkoco2cn  22717  xkoinjcn  22746  txconn  22748  imasnopn  22749  imasncld  22750  imasncls  22751  ptcmplem1  23111  ptcmplem3  23113  ptcmplem4  23114  tmdgsum2  23155  symgtgp  23165  tgpconncompeqg  23171  ghmcnp  23174  tgpt0  23178  qustgpopn  23179  qustgphaus  23182  eltsms  23192  prdsxmslem2  23591  efopn  25718  atansopn  25987  xrlimcnp  26023  fpwrelmapffslem  30969  ptrest  35703  mbfposadd  35751  cnambfre  35752  itg2addnclem2  35756  iblabsnclem  35767  ftc1anclem1  35777  ftc1anclem6  35782  pwfi2f1o  40837  smfpimioo  44208