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

Theorem f1ococnv1 6745
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 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))

Proof of Theorem f1ococnv1
StepHypRef Expression
1 f1orel 6719 . . . 4 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
2 dfrel2 6092 . . . 4 (Rel 𝐹𝐹 = 𝐹)
31, 2sylib 217 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹 = 𝐹)
43coeq2d 5771 . 2 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = (𝐹𝐹))
5 f1ocnv 6728 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
6 f1ococnv2 6743 . . 3 (𝐹:𝐵1-1-onto𝐴 → (𝐹𝐹) = ( I ↾ 𝐴))
75, 6syl 17 . 2 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
84, 7eqtr3d 2780 1 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539   I cid 5488  ccnv 5588  cres 5591  ccom 5593  Rel wrel 5594  1-1-ontowf1o 6432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440
This theorem is referenced by:  f1cocnv1  6746  f1ocnvfv1  7148  fcof1oinvd  7165  mapen  8928  mapfien  9167  hashfacen  14166  hashfacenOLD  14167  setcinv  17805  catcisolem  17825  symggrp  19008  f1omvdco2  19056  pf1mpf  21518  ufldom  23113  motgrp  26904  fmptco1f1o  30968  fcobij  31057  symgfcoeu  31351  pmtrcnel2  31359  cycpmconjslem1  31421  cycpmconjslem2  31422  reprpmtf1o  32606  subfacp1lem5  33146  ltrncoidN  38142  trlcoabs2N  38736  trlcoat  38737  trlcone  38742  cdlemg47  38750  tgrpgrplem  38763  tendoipl  38811  cdlemi2  38833  cdlemk2  38846  cdlemk4  38848  cdlemk8  38852  tendocnv  39035  dvhgrp  39121  cdlemn8  39218  dihopelvalcpre  39262  dssmap2d  41630  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614
  Copyright terms: Public domain W3C validator