Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptpreima Structured version   Visualization version   GIF version

Theorem mptpreima 5545
 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.
StepHypRef Expression
1 dmmpt.1 . . . . . 6 𝐹 = (𝑥𝐴𝐵)
2 df-mpt 4645 . . . . . 6 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
31, 2eqtri 2632 . . . . 5 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
43cnveqi 5219 . . . 4 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
5 cnvopab 5452 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
64, 5eqtri 2632 . . 3 𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
76imaeq1i 5382 . 2 (𝐹𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶)
8 df-ima 5051 . . 3 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶)
9 resopab 5366 . . . . 5 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
109rneqi 5273 . . . 4 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
11 ancom 465 . . . . . . . . 9 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶))
12 anass 679 . . . . . . . . 9 (((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1311, 12bitri 263 . . . . . . . 8 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1413exbii 1764 . . . . . . 7 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
15 19.42v 1905 . . . . . . . 8 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)))
16 df-clel 2606 . . . . . . . . . 10 (𝐵𝐶 ↔ ∃𝑦(𝑦 = 𝐵𝑦𝐶))
1716bicomi 213 . . . . . . . . 9 (∃𝑦(𝑦 = 𝐵𝑦𝐶) ↔ 𝐵𝐶)
1817anbi2i 726 . . . . . . . 8 ((𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
1915, 18bitri 263 . . . . . . 7 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
2014, 19bitri 263 . . . . . 6 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴𝐵𝐶))
2120abbii 2726 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
22 rnopab 5291 . . . . 5 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
23 df-rab 2905 . . . . 5 {𝑥𝐴𝐵𝐶} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
2421, 22, 233eqtr4i 2642 . . . 4 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥𝐴𝐵𝐶}
2510, 24eqtri 2632 . . 3 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {𝑥𝐴𝐵𝐶}
268, 25eqtri 2632 . 2 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = {𝑥𝐴𝐵𝐶}
277, 26eqtri 2632 1 (𝐹𝐶) = {𝑥𝐴𝐵𝐶}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  {crab 2900  {copab 4642   ↦ cmpt 4643  ◡ccnv 5037  ran crn 5039   ↾ cres 5040   “ cima 5041 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-xp 5044  df-rel 5045  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051 This theorem is referenced by:  mptiniseg  5546  dmmpt  5547  fmpt  6289  f1oresrab  6302  mptsuppdifd  7204  r0weon  8718  compss  9081  infrenegsup  10883  eqglact  17468  odngen  17815  psrbagsn  19316  coe1mul2lem2  19459  pjdm  19870  xkoccn  21232  txcnmpt  21237  txdis1cn  21248  pthaus  21251  txkgen  21265  xkoco1cn  21270  xkoco2cn  21271  xkoinjcn  21300  txcon  21302  imasnopn  21303  imasncld  21304  imasncls  21305  ptcmplem1  21666  ptcmplem3  21668  ptcmplem4  21669  tmdgsum2  21710  symgtgp  21715  tgpconcompeqg  21725  ghmcnp  21728  tgpt0  21732  qustgpopn  21733  qustgphaus  21736  eltsms  21746  prdsxmslem2  22144  efopn  24204  atansopn  24459  xrlimcnp  24495  fpwrelmapffslem  28895  ptrest  32578  mbfposadd  32627  cnambfre  32628  itg2addnclem2  32632  iblabsnclem  32643  ftc1anclem1  32655  ftc1anclem6  32660  pwfi2f1o  36684  smfpimioo  39672
 Copyright terms: Public domain W3C validator