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

Theorem f1ococnv1 6640
 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 6615 . . . 4 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
2 dfrel2 6044 . . . 4 (Rel 𝐹𝐹 = 𝐹)
31, 2sylib 219 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹 = 𝐹)
43coeq2d 5732 . 2 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = (𝐹𝐹))
5 f1ocnv 6624 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
6 f1ococnv2 6638 . . 3 (𝐹:𝐵1-1-onto𝐴 → (𝐹𝐹) = ( I ↾ 𝐴))
75, 6syl 17 . 2 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
84, 7eqtr3d 2863 1 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1530   I cid 5458  ◡ccnv 5553   ↾ cres 5556   ∘ ccom 5558  Rel wrel 5559  –1-1-onto→wf1o 6351 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359 This theorem is referenced by:  f1cocnv1  6641  f1ocnvfv1  7027  fcof1oinvd  7043  mapen  8670  mapfien  8860  hashfacen  13802  setcinv  17340  catcisolem  17356  symggrp  18448  f1omvdco2  18496  pf1mpf  20431  ufldom  22486  motgrp  26243  fmptco1f1o  30293  fcobij  30371  symgfcoeu  30640  pmtrcnel2  30648  cycpmconjslem1  30710  cycpmconjslem2  30711  reprpmtf1o  31783  subfacp1lem5  32315  ltrncoidN  37131  trlcoabs2N  37725  trlcoat  37726  trlcone  37731  cdlemg47  37739  tgrpgrplem  37752  tendoipl  37800  cdlemi2  37822  cdlemk2  37835  cdlemk4  37837  cdlemk8  37841  tendocnv  38024  dvhgrp  38110  cdlemn8  38207  dihopelvalcpre  38251  dssmap2d  40233  rngcinv  44084  rngcinvALTV  44096  ringcinv  44135  ringcinvALTV  44159
 Copyright terms: Public domain W3C validator