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

Theorem f1ococnv1 6328
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 6303 . . . 4 (𝐹:𝐴1-1-onto𝐵 → Rel 𝐹)
2 dfrel2 5742 . . . 4 (Rel 𝐹𝐹 = 𝐹)
31, 2sylib 208 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹 = 𝐹)
43coeq2d 5441 . 2 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = (𝐹𝐹))
5 f1ocnv 6312 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
6 f1ococnv2 6326 . . 3 (𝐹:𝐵1-1-onto𝐴 → (𝐹𝐹) = ( I ↾ 𝐴))
75, 6syl 17 . 2 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
84, 7eqtr3d 2797 1 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632   I cid 5174  ccnv 5266  cres 5269  ccom 5271  Rel wrel 5272  1-1-ontowf1o 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806  df-opab 4866  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057
This theorem is referenced by:  f1cocnv1  6329  f1ocnvfv1  6697  fcof1oinvd  6713  mapen  8292  mapfien  8481  hashfacen  13451  setcinv  16962  catcisolem  16978  symggrp  18041  f1omvdco2  18089  pf1mpf  19939  ufldom  21988  motgrp  25659  fmptco1f1o  29765  fcobij  29831  symgfcoeu  30176  reprpmtf1o  31035  subfacp1lem5  31495  ltrncoidN  35936  trlcoabs2N  36531  trlcoat  36532  trlcone  36537  cdlemg47  36545  tgrpgrplem  36558  tendoipl  36606  cdlemi2  36628  cdlemk2  36641  cdlemk4  36643  cdlemk8  36647  tendocnv  36831  dvhgrp  36917  cdlemn8  37014  dihopelvalcpre  37058  dssmap2d  38837  rngcinv  42510  rngcinvALTV  42522  ringcinv  42561  ringcinvALTV  42585
  Copyright terms: Public domain W3C validator