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

Theorem f1ococnv1 5582
Description: The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by NM, 13-Dec-2003.)
Assertion
Ref Expression
f1ococnv1  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  F )  =  (  _I  |`  A ) )

Proof of Theorem f1ococnv1
StepHypRef Expression
1 f1orel 5555 . . . 4  |-  ( F : A -1-1-onto-> B  ->  Rel  F )
2 dfrel2 5203 . . . 4  |-  ( Rel 
F  <->  `' `' F  =  F
)
31, 2sylib 188 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' `' F  =  F )
43coeq2d 4925 . 2  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  `' `' F )  =  ( `' F  o.  F
) )
5 f1ocnv 5565 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
6 f1ococnv2 5580 . . 3  |-  ( `' F : B -1-1-onto-> A  -> 
( `' F  o.  `' `' F )  =  (  _I  |`  A )
)
75, 6syl 15 . 2  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  `' `' F )  =  (  _I  |`  A )
)
84, 7eqtr3d 2392 1  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  F )  =  (  _I  |`  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    _I cid 4383   `'ccnv 4767    |` cres 4770    o. ccom 4772   Rel wrel 4773   -1-1-onto->wf1o 5333
This theorem is referenced by:  f1cocnv1  5583  f1ocnvfv1  5876  fcof1o  5887  mapen  7110  mapfien  7486  hashfacen  11482  setcinv  14015  catcisolem  14031  symggrp  14873  ufldom  17753  pf1mpf  19533  subfacp1lem5  24119  f1omvdco2  26714  ltrncoidN  30369  trlcoabs2N  30963  trlcoat  30964  trlcone  30969  cdlemg47  30977  tgrpgrplem  30990  tendoipl  31038  cdlemi2  31060  cdlemk2  31073  cdlemk4  31075  cdlemk8  31079  tendocnv  31263  dvhgrp  31349  cdlemn8  31446  dihopelvalcpre  31490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-id 4388  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341
  Copyright terms: Public domain W3C validator