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

Theorem fvimacnv 6025
Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 5683 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
Assertion
Ref Expression
fvimacnv  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( ( F `  A )  e.  B  <->  A  e.  ( `' F " B ) ) )

Proof of Theorem fvimacnv
StepHypRef Expression
1 funfvop 6022 . . . . 5  |-  ( ( Fun  F  /\  A  e.  dom  F )  ->  <. A ,  ( F `
 A ) >.  e.  F )
2 fvex 5902 . . . . . . 7  |-  ( F `
 A )  e. 
_V
3 opelcnvg 5036 . . . . . . 7  |-  ( ( ( F `  A
)  e.  _V  /\  A  e.  dom  F )  ->  ( <. ( F `  A ) ,  A >.  e.  `' F 
<-> 
<. A ,  ( F `
 A ) >.  e.  F ) )
42, 3mpan 681 . . . . . 6  |-  ( A  e.  dom  F  -> 
( <. ( F `  A ) ,  A >.  e.  `' F  <->  <. A , 
( F `  A
) >.  e.  F ) )
54adantl 472 . . . . 5  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( <. ( F `  A ) ,  A >.  e.  `' F  <->  <. A , 
( F `  A
) >.  e.  F ) )
61, 5mpbird 240 . . . 4  |-  ( ( Fun  F  /\  A  e.  dom  F )  ->  <. ( F `  A
) ,  A >.  e.  `' F )
7 elimasng 5216 . . . . . 6  |-  ( ( ( F `  A
)  e.  _V  /\  A  e.  dom  F )  ->  ( A  e.  ( `' F " { ( F `  A ) } )  <->  <. ( F `  A
) ,  A >.  e.  `' F ) )
82, 7mpan 681 . . . . 5  |-  ( A  e.  dom  F  -> 
( A  e.  ( `' F " { ( F `  A ) } )  <->  <. ( F `
 A ) ,  A >.  e.  `' F ) )
98adantl 472 . . . 4  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( A  e.  ( `' F " { ( F `  A ) } )  <->  <. ( F `
 A ) ,  A >.  e.  `' F ) )
106, 9mpbird 240 . . 3  |-  ( ( Fun  F  /\  A  e.  dom  F )  ->  A  e.  ( `' F " { ( F `
 A ) } ) )
112snss 4109 . . . . 5  |-  ( ( F `  A )  e.  B  <->  { ( F `  A ) }  C_  B )
12 imass2 5226 . . . . 5  |-  ( { ( F `  A
) }  C_  B  ->  ( `' F " { ( F `  A ) } ) 
C_  ( `' F " B ) )
1311, 12sylbi 200 . . . 4  |-  ( ( F `  A )  e.  B  ->  ( `' F " { ( F `  A ) } )  C_  ( `' F " B ) )
1413sseld 3443 . . 3  |-  ( ( F `  A )  e.  B  ->  ( A  e.  ( `' F " { ( F `
 A ) } )  ->  A  e.  ( `' F " B ) ) )
1510, 14syl5com 31 . 2  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( ( F `  A )  e.  B  ->  A  e.  ( `' F " B ) ) )
16 fvimacnvi 6024 . . . 4  |-  ( ( Fun  F  /\  A  e.  ( `' F " B ) )  -> 
( F `  A
)  e.  B )
1716ex 440 . . 3  |-  ( Fun 
F  ->  ( A  e.  ( `' F " B )  ->  ( F `  A )  e.  B ) )
1817adantr 471 . 2  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( A  e.  ( `' F " B )  ->  ( F `  A )  e.  B
) )
1915, 18impbid 195 1  |-  ( ( Fun  F  /\  A  e.  dom  F )  -> 
( ( F `  A )  e.  B  <->  A  e.  ( `' F " B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    e. wcel 1898   _Vcvv 3057    C_ wss 3416   {csn 3980   <.cop 3986   `'ccnv 4855   dom cdm 4856   "cima 4859   Fun wfun 5599   ` cfv 5605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-fv 5613
This theorem is referenced by:  funimass3  6026  elpreima  6030  iinpreima  6038  isr0  20807  rnelfmlem  21022  rnelfm  21023  fmfnfmlem2  21025  fmfnfmlem4  21027  fmfnfm  21028  metustid  21624  metustsym  21625  metustexhalf  21626  xppreima  28301  dstfrvel  29356  ballotlemrv  29402  ballotlemrvOLD  29440  grpokerinj  32229  diaintclN  34672  dibintclN  34781  dihintcl  34958  arearect  36146  areaquad  36147
  Copyright terms: Public domain W3C validator