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

Theorem f1imacnv 5764
Description: Preimage of an image. (Contributed by NM, 30-Sep-2004.)
Assertion
Ref Expression
f1imacnv  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  ( `' F " ( F " C
) )  =  C )

Proof of Theorem f1imacnv
StepHypRef Expression
1 resima 5249 . 2  |-  ( ( `' F  |`  ( F
" C ) )
" ( F " C ) )  =  ( `' F "
( F " C
) )
2 df-f1 5530 . . . . . . 7  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
32simprbi 464 . . . . . 6  |-  ( F : A -1-1-> B  ->  Fun  `' F )
43adantr 465 . . . . 5  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  Fun  `' F
)
5 funcnvres 5594 . . . . 5  |-  ( Fun  `' F  ->  `' ( F  |`  C )  =  ( `' F  |`  ( F " C
) ) )
64, 5syl 16 . . . 4  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  `' ( F  |`  C )  =  ( `' F  |`  ( F
" C ) ) )
76imaeq1d 5275 . . 3  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  ( `' ( F  |`  C ) " ( F " C ) )  =  ( ( `' F  |`  ( F " C
) ) " ( F " C ) ) )
8 f1ores 5762 . . . . 5  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  ( F  |`  C ) : C -1-1-onto-> ( F " C ) )
9 f1ocnv 5760 . . . . 5  |-  ( ( F  |`  C ) : C -1-1-onto-> ( F " C
)  ->  `' ( F  |`  C ) : ( F " C
)
-1-1-onto-> C )
108, 9syl 16 . . . 4  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  `' ( F  |`  C ) : ( F " C ) -1-1-onto-> C )
11 imadmrn 5286 . . . . 5  |-  ( `' ( F  |`  C )
" dom  `' ( F  |`  C ) )  =  ran  `' ( F  |`  C )
12 f1odm 5752 . . . . . 6  |-  ( `' ( F  |`  C ) : ( F " C ) -1-1-onto-> C  ->  dom  `' ( F  |`  C )  =  ( F " C ) )
1312imaeq2d 5276 . . . . 5  |-  ( `' ( F  |`  C ) : ( F " C ) -1-1-onto-> C  ->  ( `' ( F  |`  C )
" dom  `' ( F  |`  C ) )  =  ( `' ( F  |`  C ) " ( F " C ) ) )
14 f1ofo 5755 . . . . . 6  |-  ( `' ( F  |`  C ) : ( F " C ) -1-1-onto-> C  ->  `' ( F  |`  C ) : ( F " C
) -onto-> C )
15 forn 5730 . . . . . 6  |-  ( `' ( F  |`  C ) : ( F " C ) -onto-> C  ->  ran  `' ( F  |`  C )  =  C )
1614, 15syl 16 . . . . 5  |-  ( `' ( F  |`  C ) : ( F " C ) -1-1-onto-> C  ->  ran  `' ( F  |`  C )  =  C )
1711, 13, 163eqtr3a 2519 . . . 4  |-  ( `' ( F  |`  C ) : ( F " C ) -1-1-onto-> C  ->  ( `' ( F  |`  C )
" ( F " C ) )  =  C )
1810, 17syl 16 . . 3  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  ( `' ( F  |`  C ) " ( F " C ) )  =  C )
197, 18eqtr3d 2497 . 2  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  ( ( `' F  |`  ( F " C ) ) "
( F " C
) )  =  C )
201, 19syl5eqr 2509 1  |-  ( ( F : A -1-1-> B  /\  C  C_  A )  ->  ( `' F " ( F " C
) )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    C_ wss 3435   `'ccnv 4946   dom cdm 4947   ran crn 4948    |` cres 4949   "cima 4950   Fun wfun 5519   -->wf 5521   -1-1->wf1 5522   -onto->wfo 5523   -1-1-onto->wf1o 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532
This theorem is referenced by:  f1opw2  6422  ssenen  7594  f1opwfi  7725  isf34lem3  8654  subggim  15912  gicsubgen  15924  cnt1  19085  basqtop  19415  tgqtop  19416  hmeoopn  19470  hmeocld  19471  hmeontr  19473  qtopf1  19520  f1otrg  23268  tpr2rico  26486  eulerpartlemmf  26901  ballotlemscr  27044  ballotlemrinv0  27058  cvmlift2lem9a  27335  grpokerinj  28897
  Copyright terms: Public domain W3C validator