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

Theorem foimacnv 5772
Description: A reverse version of f1imacnv 5771. (Contributed by Jeff Hankins, 16-Jul-2009.)
Assertion
Ref Expression
foimacnv  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ( F "
( `' F " C ) )  =  C )

Proof of Theorem foimacnv
StepHypRef Expression
1 resima 5247 . 2  |-  ( ( F  |`  ( `' F " C ) )
" ( `' F " C ) )  =  ( F " ( `' F " C ) )
2 fofun 5735 . . . . . 6  |-  ( F : A -onto-> B  ->  Fun  F )
32adantr 463 . . . . 5  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  Fun  F )
4 funcnvres2 5596 . . . . 5  |-  ( Fun 
F  ->  `' ( `' F  |`  C )  =  ( F  |`  ( `' F " C ) ) )
53, 4syl 17 . . . 4  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  `' ( `' F  |`  C )  =  ( F  |`  ( `' F " C ) ) )
65imaeq1d 5277 . . 3  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ( `' ( `' F  |`  C )
" ( `' F " C ) )  =  ( ( F  |`  ( `' F " C ) ) " ( `' F " C ) ) )
7 resss 5238 . . . . . . . . . . 11  |-  ( `' F  |`  C )  C_  `' F
8 cnvss 5117 . . . . . . . . . . 11  |-  ( ( `' F  |`  C ) 
C_  `' F  ->  `' ( `' F  |`  C )  C_  `' `' F )
97, 8ax-mp 5 . . . . . . . . . 10  |-  `' ( `' F  |`  C ) 
C_  `' `' F
10 cnvcnvss 5399 . . . . . . . . . 10  |-  `' `' F  C_  F
119, 10sstri 3450 . . . . . . . . 9  |-  `' ( `' F  |`  C ) 
C_  F
12 funss 5543 . . . . . . . . 9  |-  ( `' ( `' F  |`  C )  C_  F  ->  ( Fun  F  ->  Fun  `' ( `' F  |`  C ) ) )
1311, 2, 12mpsyl 62 . . . . . . . 8  |-  ( F : A -onto-> B  ->  Fun  `' ( `' F  |`  C ) )
1413adantr 463 . . . . . . 7  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  Fun  `' ( `' F  |`  C ) )
15 df-ima 4955 . . . . . . . 8  |-  ( `' F " C )  =  ran  ( `' F  |`  C )
16 df-rn 4953 . . . . . . . 8  |-  ran  ( `' F  |`  C )  =  dom  `' ( `' F  |`  C )
1715, 16eqtr2i 2432 . . . . . . 7  |-  dom  `' ( `' F  |`  C )  =  ( `' F " C )
1814, 17jctir 536 . . . . . 6  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ( Fun  `' ( `' F  |`  C )  /\  dom  `' ( `' F  |`  C )  =  ( `' F " C ) ) )
19 df-fn 5528 . . . . . 6  |-  ( `' ( `' F  |`  C )  Fn  ( `' F " C )  <-> 
( Fun  `' ( `' F  |`  C )  /\  dom  `' ( `' F  |`  C )  =  ( `' F " C ) ) )
2018, 19sylibr 212 . . . . 5  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  `' ( `' F  |`  C )  Fn  ( `' F " C ) )
21 dfdm4 5137 . . . . . 6  |-  dom  ( `' F  |`  C )  =  ran  `' ( `' F  |`  C )
22 forn 5737 . . . . . . . . . 10  |-  ( F : A -onto-> B  ->  ran  F  =  B )
2322sseq2d 3469 . . . . . . . . 9  |-  ( F : A -onto-> B  -> 
( C  C_  ran  F  <-> 
C  C_  B )
)
2423biimpar 483 . . . . . . . 8  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  C  C_  ran  F )
25 df-rn 4953 . . . . . . . 8  |-  ran  F  =  dom  `' F
2624, 25syl6sseq 3487 . . . . . . 7  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  C  C_  dom  `' F )
27 ssdmres 5236 . . . . . . 7  |-  ( C 
C_  dom  `' F  <->  dom  ( `' F  |`  C )  =  C )
2826, 27sylib 196 . . . . . 6  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  dom  ( `' F  |`  C )  =  C )
2921, 28syl5eqr 2457 . . . . 5  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ran  `' ( `' F  |`  C )  =  C )
30 df-fo 5531 . . . . 5  |-  ( `' ( `' F  |`  C ) : ( `' F " C )
-onto-> C  <->  ( `' ( `' F  |`  C )  Fn  ( `' F " C )  /\  ran  `' ( `' F  |`  C )  =  C ) )
3120, 29, 30sylanbrc 662 . . . 4  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  `' ( `' F  |`  C ) : ( `' F " C ) -onto-> C )
32 foima 5739 . . . 4  |-  ( `' ( `' F  |`  C ) : ( `' F " C )
-onto-> C  ->  ( `' ( `' F  |`  C )
" ( `' F " C ) )  =  C )
3331, 32syl 17 . . 3  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ( `' ( `' F  |`  C )
" ( `' F " C ) )  =  C )
346, 33eqtr3d 2445 . 2  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ( ( F  |`  ( `' F " C ) ) "
( `' F " C ) )  =  C )
351, 34syl5eqr 2457 1  |-  ( ( F : A -onto-> B  /\  C  C_  B )  ->  ( F "
( `' F " C ) )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    C_ wss 3413   `'ccnv 4941   dom cdm 4942   ran crn 4943    |` cres 4944   "cima 4945   Fun wfun 5519    Fn wfn 5520   -onto->wfo 5523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-id 4737  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-fun 5527  df-fn 5528  df-f 5529  df-fo 5531
This theorem is referenced by:  f1opw2  6465  imacosupp  6897  fopwdom  7583  f1opwfi  7778  enfin2i  8653  fin1a2lem7  8738  fsumss  13603  fprodss  13814  gicsubgen  16542  gsumval3OLD  17124  coe1mul2lem2  18521  cncmp  20077  cnconn  20107  qtoprest  20402  qtopomap  20403  qtopcmap  20404  hmeoimaf1o  20455  elfm3  20635  imasf1oxms  21176  mbfimaopnlem  22246  cvmsss2  29452  diaintclN  34059  dibintclN  34168  dihintcl  34345  lnmepi  35374  pwfi2f1o  35387  pwfi2f1oOLD  35388
  Copyright terms: Public domain W3C validator