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

Theorem mptpreima 6070
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 5111 . . . . . 6 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
31, 2eqtri 2761 . . . . 5 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
43cnveqi 5717 . . . 4 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
5 cnvopab 5971 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
64, 5eqtri 2761 . . 3 𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
76imaeq1i 5900 . 2 (𝐹𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶)
8 df-ima 5538 . . 3 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶)
9 resopab 5876 . . . . 5 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
109rneqi 5780 . . . 4 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
11 ancom 464 . . . . . . . . 9 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶))
12 anass 472 . . . . . . . . 9 (((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1311, 12bitri 278 . . . . . . . 8 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1413exbii 1854 . . . . . . 7 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
15 19.42v 1961 . . . . . . . 8 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)))
16 dfclel 2812 . . . . . . . . . 10 (𝐵𝐶 ↔ ∃𝑦(𝑦 = 𝐵𝑦𝐶))
1716bicomi 227 . . . . . . . . 9 (∃𝑦(𝑦 = 𝐵𝑦𝐶) ↔ 𝐵𝐶)
1817anbi2i 626 . . . . . . . 8 ((𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
1915, 18bitri 278 . . . . . . 7 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
2014, 19bitri 278 . . . . . 6 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴𝐵𝐶))
2120abbii 2803 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
22 rnopab 5797 . . . . 5 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
23 df-rab 3062 . . . . 5 {𝑥𝐴𝐵𝐶} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
2421, 22, 233eqtr4i 2771 . . . 4 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥𝐴𝐵𝐶}
2510, 24eqtri 2761 . . 3 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {𝑥𝐴𝐵𝐶}
268, 25eqtri 2761 . 2 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = {𝑥𝐴𝐵𝐶}
277, 26eqtri 2761 1 (𝐹𝐶) = {𝑥𝐴𝐵𝐶}
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1542  wex 1786  wcel 2114  {cab 2716  {crab 3057  {copab 5092  cmpt 5110  ccnv 5524  ran crn 5526  cres 5527  cima 5528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-mpt 5111  df-xp 5531  df-rel 5532  df-cnv 5533  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538
This theorem is referenced by:  mptiniseg  6071  dmmpt  6072  fmpt  6884  f1oresrab  6899  mptsuppdifd  7881  r0weon  9512  compss  9876  infrenegsup  11701  eqglact  18449  odngen  18820  pjdm  20523  psrbagsn  20875  coe1mul2lem2  21043  xkoccn  22370  txcnmpt  22375  txdis1cn  22386  pthaus  22389  txkgen  22403  xkoco1cn  22408  xkoco2cn  22409  xkoinjcn  22438  txconn  22440  imasnopn  22441  imasncld  22442  imasncls  22443  ptcmplem1  22803  ptcmplem3  22805  ptcmplem4  22806  tmdgsum2  22847  symgtgp  22857  tgpconncompeqg  22863  ghmcnp  22866  tgpt0  22870  qustgpopn  22871  qustgphaus  22874  eltsms  22884  prdsxmslem2  23282  efopn  25401  atansopn  25670  xrlimcnp  25706  fpwrelmapffslem  30642  ptrest  35399  mbfposadd  35447  cnambfre  35448  itg2addnclem2  35452  iblabsnclem  35463  ftc1anclem1  35473  ftc1anclem6  35478  pwfi2f1o  40493  smfpimioo  43860
  Copyright terms: Public domain W3C validator