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

Theorem f1ococnv1 5669
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 5644 . . . 4  |-  ( F : A -1-1-onto-> B  ->  Rel  F )
2 dfrel2 5288 . . . 4  |-  ( Rel 
F  <->  `' `' F  =  F
)
31, 2sylib 196 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' `' F  =  F )
43coeq2d 5002 . 2  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  `' `' F )  =  ( `' F  o.  F
) )
5 f1ocnv 5653 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
6 f1ococnv2 5667 . . 3  |-  ( `' F : B -1-1-onto-> A  -> 
( `' F  o.  `' `' F )  =  (  _I  |`  A )
)
75, 6syl 16 . 2  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  `' `' F )  =  (  _I  |`  A )
)
84, 7eqtr3d 2477 1  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  F )  =  (  _I  |`  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    _I cid 4631   `'ccnv 4839    |` cres 4842    o. ccom 4844   Rel wrel 4845   -1-1-onto->wf1o 5417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425
This theorem is referenced by:  f1cocnv1  5670  f1ocnvfv1  5983  fcof1o  5997  mapen  7475  mapfien  7657  mapfienOLD  7927  hashfacen  12207  setcinv  14958  catcisolem  14974  symggrp  15905  f1omvdco2  15954  pf1mpf  17786  ufldom  19535  fcobij  26025  subfacp1lem5  27072  ltrncoidN  33772  trlcoabs2N  34366  trlcoat  34367  trlcone  34372  cdlemg47  34380  tgrpgrplem  34393  tendoipl  34441  cdlemi2  34463  cdlemk2  34476  cdlemk4  34478  cdlemk8  34482  tendocnv  34666  dvhgrp  34752  cdlemn8  34849  dihopelvalcpre  34893
  Copyright terms: Public domain W3C validator