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

Theorem f1ococnv1 5686
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

Proof of Theorem f1ococnv1
StepHypRef Expression
1 f1orel 5661 . . . 4
2 dfrel2 5308 . . . 4
31, 2sylib 190 . . 3
43coeq2d 5024 . 2
5 f1ocnv 5670 . . 3
6 f1ococnv2 5684 . . 3
75, 6syl 16 . 2
84, 7eqtr3d 2523 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1670   cid 4652  `'ccnv 4861  |`cres 4864  o.ccom 4866  Relwrel 4867  -1-1-onto->wf1o 5437
This theorem is referenced by:  f1cocnv1  5687  f1ocnvfv1  5995  fcof1o  6007  mapen  7436  mapfien  7820  hashfacen  12054  setcinv  14799  catcisolem  14815  symggrp  15686  f1omvdco2  17605  ufldom  19009  pf1mpf  20987  fcobij  25155  subfacp1lem5  26218  ltrncoidN  32475  trlcoabs2N  33069  trlcoat  33070  trlcone  33075  cdlemg47  33083  tgrpgrplem  33096  tendoipl  33144  cdlemi2  33166  cdlemk2  33179  cdlemk4  33181  cdlemk8  33185  tendocnv  33369  dvhgrp  33455  cdlemn8  33552  dihopelvalcpre  33596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-br 4319  df-opab 4377  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445
  Copyright terms: Public domain W3C validator