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

Theorem mptpreima 6194
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 5193 . . . . . 6 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
31, 2eqtri 2761 . . . . 5 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
43cnveqi 5834 . . . 4 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
5 cnvopab 6095 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
64, 5eqtri 2761 . . 3 𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
76imaeq1i 6014 . 2 (𝐹𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶)
8 df-ima 5650 . . 3 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶)
9 resopab 5992 . . . . 5 ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
109rneqi 5896 . . . 4 ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
11 ancom 462 . . . . . . . . 9 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶))
12 anass 470 . . . . . . . . 9 (((𝑥𝐴𝑦 = 𝐵) ∧ 𝑦𝐶) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1311, 12bitri 275 . . . . . . . 8 ((𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
1413exbii 1851 . . . . . . 7 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ ∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)))
15 19.42v 1958 . . . . . . . 8 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)))
16 dfclel 2812 . . . . . . . . . 10 (𝐵𝐶 ↔ ∃𝑦(𝑦 = 𝐵𝑦𝐶))
1716bicomi 223 . . . . . . . . 9 (∃𝑦(𝑦 = 𝐵𝑦𝐶) ↔ 𝐵𝐶)
1817anbi2i 624 . . . . . . . 8 ((𝑥𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
1915, 18bitri 275 . . . . . . 7 (∃𝑦(𝑥𝐴 ∧ (𝑦 = 𝐵𝑦𝐶)) ↔ (𝑥𝐴𝐵𝐶))
2014, 19bitri 275 . . . . . 6 (∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵)) ↔ (𝑥𝐴𝐵𝐶))
2120abbii 2803 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ (𝑥𝐴𝐵𝐶)}
22 rnopab 5913 . . . . 5 ran {⟨𝑦, 𝑥⟩ ∣ (𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦𝐶 ∧ (𝑥𝐴𝑦 = 𝐵))}
23 df-rab 3407 . . . . 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 397   = wceq 1542  wex 1782  wcel 2107  {cab 2710  {crab 3406  {copab 5171  cmpt 5192  ccnv 5636  ran crn 5638  cres 5639  cima 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110  df-opab 5172  df-mpt 5193  df-xp 5643  df-rel 5644  df-cnv 5645  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650
This theorem is referenced by:  mptiniseg  6195  dmmpt  6196  fmpt  7062  f1oresrab  7077  mptsuppdifd  8121  r0weon  9956  compss  10320  infrenegsup  12146  eqglact  18989  odngen  19367  pjdm  21136  psrbagsn  21494  coe1mul2lem2  21662  xkoccn  22993  txcnmpt  22998  txdis1cn  23009  pthaus  23012  txkgen  23026  xkoco1cn  23031  xkoco2cn  23032  xkoinjcn  23061  txconn  23063  imasnopn  23064  imasncld  23065  imasncls  23066  ptcmplem1  23426  ptcmplem3  23428  ptcmplem4  23429  tmdgsum2  23470  symgtgp  23480  tgpconncompeqg  23486  ghmcnp  23489  tgpt0  23493  qustgpopn  23494  qustgphaus  23497  eltsms  23507  prdsxmslem2  23908  efopn  26036  atansopn  26305  xrlimcnp  26341  fpwrelmapffslem  31703  ptrest  36127  mbfposadd  36175  cnambfre  36176  itg2addnclem2  36180  iblabsnclem  36191  ftc1anclem1  36201  ftc1anclem6  36206  pwfi2f1o  41470  smfpimioo  45118
  Copyright terms: Public domain W3C validator