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

Theorem fimacnv 6004
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 5339 . . 3  |-  ( `' F " B ) 
C_  ran  `' F
2 dfdm4 5186 . . . 4  |-  dom  F  =  ran  `' F
3 fdm 5726 . . . . 5  |-  ( F : A --> B  ->  dom  F  =  A )
4 ssid 3516 . . . . 5  |-  A  C_  A
53, 4syl6eqss 3547 . . . 4  |-  ( F : A --> B  ->  dom  F  C_  A )
62, 5syl5eqssr 3542 . . 3  |-  ( F : A --> B  ->  ran  `' F  C_  A )
71, 6syl5ss 3508 . 2  |-  ( F : A --> B  -> 
( `' F " B )  C_  A
)
8 imassrn 5339 . . . 4  |-  ( F
" A )  C_  ran  F
9 frn 5728 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
108, 9syl5ss 3508 . . 3  |-  ( F : A --> B  -> 
( F " A
)  C_  B )
11 ffun 5724 . . . 4  |-  ( F : A --> B  ->  Fun  F )
124, 3syl5sseqr 3546 . . . 4  |-  ( F : A --> B  ->  A  C_  dom  F )
13 funimass3 5988 . . . 4  |-  ( ( Fun  F  /\  A  C_ 
dom  F )  -> 
( ( F " A )  C_  B  <->  A 
C_  ( `' F " B ) ) )
1411, 12, 13syl2anc 661 . . 3  |-  ( F : A --> B  -> 
( ( F " A )  C_  B  <->  A 
C_  ( `' F " B ) ) )
1510, 14mpbid 210 . 2  |-  ( F : A --> B  ->  A  C_  ( `' F " B ) )
167, 15eqssd 3514 1  |-  ( F : A --> B  -> 
( `' F " B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374    C_ wss 3469   `'ccnv 4991   dom cdm 4992   ran crn 4993   "cima 4995   Fun wfun 5573   -->wf 5575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587
This theorem is referenced by:  fmpt  6033  frnsuppeq  6903  fin1a2lem7  8775  nn0suppOLD  10839  cnclima  19528  iscncl  19529  cnindis  19552  cncmp  19651  ptrescn  19868  qtopuni  19931  qtopcld  19942  qtopcmap  19948  ordthmeolem  20030  rnelfmlem  20181  mbfdm  21763  ismbf  21765  mbfimaicc  21768  ismbf2d  21776  ismbf3d  21789  mbfimaopn2  21792  i1fd  21816  plyeq0  22336  fimacnvinrn  26998  fsumcvg4  27418  zrhunitpreima  27445  imambfm  27723  dstrvprob  27900  dvtanlem  29492  dvtan  29493  fsuppeq  30500
  Copyright terms: Public domain W3C validator