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

Theorem mptpreima 5354
Description: The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
Hypothesis
Ref Expression
dmmpt2.1  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
mptpreima  |-  ( `' F " C )  =  { x  e.  A  |  B  e.  C }
Distinct variable group:    x, C
Allowed substitution hints:    A( x)    B( x)    F( x)

Proof of Theorem mptpreima
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dmmpt2.1 . . . . . 6  |-  F  =  ( x  e.  A  |->  B )
2 df-mpt 4260 . . . . . 6  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
31, 2eqtri 2455 . . . . 5  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
43cnveqi 5038 . . . 4  |-  `' F  =  `' { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
5 cnvopab 5265 . . . 4  |-  `' { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }  =  { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }
64, 5eqtri 2455 . . 3  |-  `' F  =  { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }
76imaeq1i 5191 . 2  |-  ( `' F " C )  =  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) } " C )
8 df-ima 4882 . . 3  |-  ( {
<. y ,  x >.  |  ( x  e.  A  /\  y  =  B
) } " C
)  =  ran  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }  |`  C )
9 resopab 5178 . . . . 5  |-  ( {
<. y ,  x >.  |  ( x  e.  A  /\  y  =  B
) }  |`  C )  =  { <. y ,  x >.  |  (
y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }
109rneqi 5087 . . . 4  |-  ran  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }  |`  C )  =  ran  { <. y ,  x >.  |  ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }
11 ancom 438 . . . . . . . . 9  |-  ( ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) )  <->  ( (
x  e.  A  /\  y  =  B )  /\  y  e.  C
) )
12 anass 631 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  =  B
)  /\  y  e.  C )  <->  ( x  e.  A  /\  (
y  =  B  /\  y  e.  C )
) )
1311, 12bitri 241 . . . . . . . 8  |-  ( ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) )  <->  ( x  e.  A  /\  (
y  =  B  /\  y  e.  C )
) )
1413exbii 1592 . . . . . . 7  |-  ( E. y ( y  e.  C  /\  ( x  e.  A  /\  y  =  B ) )  <->  E. y
( x  e.  A  /\  ( y  =  B  /\  y  e.  C
) ) )
15 19.42v 1928 . . . . . . . 8  |-  ( E. y ( x  e.  A  /\  ( y  =  B  /\  y  e.  C ) )  <->  ( x  e.  A  /\  E. y
( y  =  B  /\  y  e.  C
) ) )
16 df-clel 2431 . . . . . . . . . 10  |-  ( B  e.  C  <->  E. y
( y  =  B  /\  y  e.  C
) )
1716bicomi 194 . . . . . . . . 9  |-  ( E. y ( y  =  B  /\  y  e.  C )  <->  B  e.  C )
1817anbi2i 676 . . . . . . . 8  |-  ( ( x  e.  A  /\  E. y ( y  =  B  /\  y  e.  C ) )  <->  ( x  e.  A  /\  B  e.  C ) )
1915, 18bitri 241 . . . . . . 7  |-  ( E. y ( x  e.  A  /\  ( y  =  B  /\  y  e.  C ) )  <->  ( x  e.  A  /\  B  e.  C ) )
2014, 19bitri 241 . . . . . 6  |-  ( E. y ( y  e.  C  /\  ( x  e.  A  /\  y  =  B ) )  <->  ( x  e.  A  /\  B  e.  C ) )
2120abbii 2547 . . . . 5  |-  { x  |  E. y ( y  e.  C  /\  (
x  e.  A  /\  y  =  B )
) }  =  {
x  |  ( x  e.  A  /\  B  e.  C ) }
22 rnopab 5106 . . . . 5  |-  ran  { <. y ,  x >.  |  ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }  =  { x  |  E. y ( y  e.  C  /\  ( x  e.  A  /\  y  =  B ) ) }
23 df-rab 2706 . . . . 5  |-  { x  e.  A  |  B  e.  C }  =  {
x  |  ( x  e.  A  /\  B  e.  C ) }
2421, 22, 233eqtr4i 2465 . . . 4  |-  ran  { <. y ,  x >.  |  ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }  =  { x  e.  A  |  B  e.  C }
2510, 24eqtri 2455 . . 3  |-  ran  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }  |`  C )  =  { x  e.  A  |  B  e.  C }
268, 25eqtri 2455 . 2  |-  ( {
<. y ,  x >.  |  ( x  e.  A  /\  y  =  B
) } " C
)  =  { x  e.  A  |  B  e.  C }
277, 26eqtri 2455 1  |-  ( `' F " C )  =  { x  e.  A  |  B  e.  C }
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1550    = wceq 1652    e. wcel 1725   {cab 2421   {crab 2701   {copab 4257    e. cmpt 4258   `'ccnv 4868   ran crn 4870    |` cres 4871   "cima 4872
This theorem is referenced by:  mptiniseg  5355  dmmpt  5356  fmpt  5881  suppss2  6291  suppssfv  6292  suppssov1  6293  cantnfreslem  7620  cantnfres  7622  cantnflem1  7634  cantnf  7638  r0weon  7883  compss  8245  infmsup  9975  eqglact  14979  odngen  15199  rrgsupp  16339  psrbagsn  16543  coe1mul2lem2  16649  pjdm  16922  xkoccn  17639  txcnmpt  17644  txdis1cn  17655  pthaus  17658  txkgen  17672  xkoco1cn  17677  xkoco2cn  17678  xkoinjcn  17707  txcon  17709  imasnopn  17710  imasncld  17711  imasncls  17712  ptcmplem1  18071  ptcmplem3  18073  ptcmplem4  18074  tmdgsum2  18114  symgtgp  18119  tgpconcompeqg  18129  ghmcnp  18132  tgpt0  18136  divstgpopn  18137  divstgphaus  18140  eltsms  18150  prdsxmslem2  18547  efopn  20537  atansopn  20760  xrlimcnp  20795  lgseisenlem3  21123  lgseisenlem4  21124  suppss2f  24037  mbfposadd  26200  cnambfre  26201  itg2addnclem2  26203  iblabsnclem  26214  uvcff  27155  pwfi2f1o  27175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-mpt 4260  df-xp 4875  df-rel 4876  df-cnv 4877  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882
  Copyright terms: Public domain W3C validator