ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mptpreima Unicode version

Theorem mptpreima 5114
Description: The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
Hypothesis
Ref Expression
dmmpo.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 dmmpo.1 . . . . . 6  |-  F  =  ( x  e.  A  |->  B )
2 df-mpt 4061 . . . . . 6  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
31, 2eqtri 2196 . . . . 5  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
43cnveqi 4795 . . . 4  |-  `' F  =  `' { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
5 cnvopab 5022 . . . 4  |-  `' { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }  =  { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }
64, 5eqtri 2196 . . 3  |-  `' F  =  { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }
76imaeq1i 4960 . 2  |-  ( `' F " C )  =  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) } " C )
8 df-ima 4633 . . 3  |-  ( {
<. y ,  x >.  |  ( x  e.  A  /\  y  =  B
) } " C
)  =  ran  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }  |`  C )
9 resopab 4944 . . . . 5  |-  ( {
<. y ,  x >.  |  ( x  e.  A  /\  y  =  B
) }  |`  C )  =  { <. y ,  x >.  |  (
y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }
109rneqi 4848 . . . 4  |-  ran  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }  |`  C )  =  ran  { <. y ,  x >.  |  ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }
11 ancom 266 . . . . . . . . 9  |-  ( ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) )  <->  ( (
x  e.  A  /\  y  =  B )  /\  y  e.  C
) )
12 anass 401 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  =  B
)  /\  y  e.  C )  <->  ( x  e.  A  /\  (
y  =  B  /\  y  e.  C )
) )
1311, 12bitri 184 . . . . . . . 8  |-  ( ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) )  <->  ( x  e.  A  /\  (
y  =  B  /\  y  e.  C )
) )
1413exbii 1603 . . . . . . 7  |-  ( E. y ( y  e.  C  /\  ( x  e.  A  /\  y  =  B ) )  <->  E. y
( x  e.  A  /\  ( y  =  B  /\  y  e.  C
) ) )
15 19.42v 1904 . . . . . . . 8  |-  ( E. y ( x  e.  A  /\  ( y  =  B  /\  y  e.  C ) )  <->  ( x  e.  A  /\  E. y
( y  =  B  /\  y  e.  C
) ) )
16 df-clel 2171 . . . . . . . . . 10  |-  ( B  e.  C  <->  E. y
( y  =  B  /\  y  e.  C
) )
1716bicomi 132 . . . . . . . . 9  |-  ( E. y ( y  =  B  /\  y  e.  C )  <->  B  e.  C )
1817anbi2i 457 . . . . . . . 8  |-  ( ( x  e.  A  /\  E. y ( y  =  B  /\  y  e.  C ) )  <->  ( x  e.  A  /\  B  e.  C ) )
1915, 18bitri 184 . . . . . . 7  |-  ( E. y ( x  e.  A  /\  ( y  =  B  /\  y  e.  C ) )  <->  ( x  e.  A  /\  B  e.  C ) )
2014, 19bitri 184 . . . . . 6  |-  ( E. y ( y  e.  C  /\  ( x  e.  A  /\  y  =  B ) )  <->  ( x  e.  A  /\  B  e.  C ) )
2120abbii 2291 . . . . 5  |-  { x  |  E. y ( y  e.  C  /\  (
x  e.  A  /\  y  =  B )
) }  =  {
x  |  ( x  e.  A  /\  B  e.  C ) }
22 rnopab 4867 . . . . 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 2462 . . . . 5  |-  { x  e.  A  |  B  e.  C }  =  {
x  |  ( x  e.  A  /\  B  e.  C ) }
2421, 22, 233eqtr4i 2206 . . . 4  |-  ran  { <. y ,  x >.  |  ( y  e.  C  /\  ( x  e.  A  /\  y  =  B
) ) }  =  { x  e.  A  |  B  e.  C }
2510, 24eqtri 2196 . . 3  |-  ran  ( { <. y ,  x >.  |  ( x  e.  A  /\  y  =  B ) }  |`  C )  =  { x  e.  A  |  B  e.  C }
268, 25eqtri 2196 . 2  |-  ( {
<. y ,  x >.  |  ( x  e.  A  /\  y  =  B
) } " C
)  =  { x  e.  A  |  B  e.  C }
277, 26eqtri 2196 1  |-  ( `' F " C )  =  { x  e.  A  |  B  e.  C }
Colors of variables: wff set class
Syntax hints:    /\ wa 104    = wceq 1353   E.wex 1490    e. wcel 2146   {cab 2161   {crab 2457   {copab 4058    |-> cmpt 4059   `'ccnv 4619   ran crn 4621    |` cres 4622   "cima 4623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999  df-opab 4060  df-mpt 4061  df-xp 4626  df-rel 4627  df-cnv 4628  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633
This theorem is referenced by:  mptiniseg  5115  dmmpt  5116  fmpt  5658  f1oresrab  5673  suppssfv  6069  suppssov1  6070  infrenegsupex  9567  infxrnegsupex  11239  txcnmpt  13353  txdis1cn  13358  imasnopn  13379
  Copyright terms: Public domain W3C validator