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

Theorem fimacnv 5971
Description: The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
Assertion
Ref Expression
fimacnv  |-  ( F : A --> B  -> 
( `' F " B )  =  A )

Proof of Theorem fimacnv
StepHypRef Expression
1 imassrn 5141 . . 3  |-  ( `' F " B ) 
C_  ran  `' F
2 dfdm4 4989 . . . 4  |-  dom  F  =  ran  `' F
3 fdm 5693 . . . . 5  |-  ( F : A --> B  ->  dom  F  =  A )
4 ssid 3426 . . . . 5  |-  A  C_  A
53, 4syl6eqss 3457 . . . 4  |-  ( F : A --> B  ->  dom  F  C_  A )
62, 5syl5eqssr 3452 . . 3  |-  ( F : A --> B  ->  ran  `' F  C_  A )
71, 6syl5ss 3418 . 2  |-  ( F : A --> B  -> 
( `' F " B )  C_  A
)
8 imassrn 5141 . . . 4  |-  ( F
" A )  C_  ran  F
9 frn 5695 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
108, 9syl5ss 3418 . . 3  |-  ( F : A --> B  -> 
( F " A
)  C_  B )
11 ffun 5691 . . . 4  |-  ( F : A --> B  ->  Fun  F )
124, 3syl5sseqr 3456 . . . 4  |-  ( F : A --> B  ->  A  C_  dom  F )
13 funimass3 5957 . . . 4  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( ( F " A )  C_  B  <->  A 
C_  ( `' F " B ) ) )
1411, 12, 13syl2anc 665 . . 3  |-  ( F : A --> B  -> 
( ( F " A )  C_  B  <->  A 
C_  ( `' F " B ) ) )
1510, 14mpbid 213 . 2  |-  ( F : A --> B  ->  A  C_  ( `' F " B ) )
167, 15eqssd 3424 1  |-  ( F : A --> B  -> 
( `' F " B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    C_ wss 3379   `'ccnv 4795   dom cdm 4796   ran crn 4797   "cima 4799   Fun wfun 5538   -->wf 5540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-fv 5552
This theorem is referenced by:  fmpt  6002  frnsuppeq  6881  fin1a2lem7  8787  cnclima  20226  iscncl  20227  cnindis  20250  cncmp  20349  ptrescn  20596  qtopuni  20659  qtopcld  20670  qtopcmap  20676  ordthmeolem  20758  rnelfmlem  20909  mbfdm  22526  ismbf  22528  mbfimaicc  22531  ismbf2d  22539  ismbf3d  22552  mbfimaopn2  22555  i1fd  22581  plyeq0  23107  fimacnvinrn  28181  fsumcvg4  28708  zrhunitpreima  28734  imambfm  29036  carsggect  29102  dstrvprob  29256  poimirlem30  31877  dvtanlemOLD  31898  dvtan  31899
  Copyright terms: Public domain W3C validator