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

Theorem mptpreima 5592
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 4680 . . . . . 6 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
31, 2eqtri 2643 . . . . 5 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
43cnveqi 5262 . . . 4 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
5 cnvopab 5497 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
64, 5eqtri 2643 . . 3 𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
76imaeq1i 5427 . 2 (𝐹𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶)
8 df-ima 5092 . . 3 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶)
9 resopab 5410 . . . . 5 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
109rneqi 5317 . . . 4 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
11 ancom 466 . . . . . . . . 9 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶))
12 anass 680 . . . . . . . . 9 (((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1311, 12bitri 264 . . . . . . . 8 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1413exbii 1771 . . . . . . 7 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
15 19.42v 1915 . . . . . . . 8 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)))
16 df-clel 2617 . . . . . . . . . 10 (𝐵𝐶 ↔ ∃𝑦(𝑦 = 𝐵𝑦𝐶))
1716bicomi 214 . . . . . . . . 9 (∃𝑦(𝑦 = 𝐵𝑦𝐶) ↔ 𝐵𝐶)
1817anbi2i 729 . . . . . . . 8 ((𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
1915, 18bitri 264 . . . . . . 7 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
2014, 19bitri 264 . . . . . 6 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴𝐵𝐶))
2120abbii 2736 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
22 rnopab 5335 . . . . 5 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
23 df-rab 2916 . . . . 5 {𝑥𝐴𝐵𝐶} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
2421, 22, 233eqtr4i 2653 . . . 4 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥𝐴𝐵𝐶}
2510, 24eqtri 2643 . . 3 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {𝑥𝐴𝐵𝐶}
268, 25eqtri 2643 . 2 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = {𝑥𝐴𝐵𝐶}
277, 26eqtri 2643 1 (𝐹𝐶) = {𝑥𝐴𝐵𝐶}
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1480  wex 1701  wcel 1987  {cab 2607  {crab 2911  {copab 4677  cmpt 4678  ccnv 5078  ran crn 5080  cres 5081  cima 5082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-opab 4679  df-mpt 4680  df-xp 5085  df-rel 5086  df-cnv 5087  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092
This theorem is referenced by:  mptiniseg  5593  dmmpt  5594  fmpt  6342  f1oresrab  6356  mptsuppdifd  7269  r0weon  8787  compss  9150  infrenegsup  10958  eqglact  17577  odngen  17924  psrbagsn  19427  coe1mul2lem2  19570  pjdm  19983  xkoccn  21345  txcnmpt  21350  txdis1cn  21361  pthaus  21364  txkgen  21378  xkoco1cn  21383  xkoco2cn  21384  xkoinjcn  21413  txconn  21415  imasnopn  21416  imasncld  21417  imasncls  21418  ptcmplem1  21779  ptcmplem3  21781  ptcmplem4  21782  tmdgsum2  21823  symgtgp  21828  tgpconncompeqg  21838  ghmcnp  21841  tgpt0  21845  qustgpopn  21846  qustgphaus  21849  eltsms  21859  prdsxmslem2  22257  efopn  24321  atansopn  24576  xrlimcnp  24612  fpwrelmapffslem  29373  ptrest  33075  mbfposadd  33124  cnambfre  33125  itg2addnclem2  33129  iblabsnclem  33140  ftc1anclem1  33152  ftc1anclem6  33157  pwfi2f1o  37181  smfpimioo  40327
  Copyright terms: Public domain W3C validator