Theorem f1ococnv1 6877

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

Step	Hyp	Ref	Expression
1		f1orel 6851	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6210	. . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3	1, 2	sylib 218	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡◡𝐹 = 𝐹)
4	3	coeq2d 5875	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = (◡𝐹 ∘ 𝐹))
5		f1ocnv 6860	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6875	. . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴))
7	5, 6	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴))
8	4, 7	eqtr3d 2776	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

Syntax hints:   → wi 4   = wceq 1536   I cid 5581  ^◡ccnv 5687   ↾ cres 5690   ∘ ccom 5692  Rel wrel 5693  –1-1-onto→wf1o 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569

This theorem is referenced by:  f1cocnv1  6878  f1ocnvfv1  7295  fcof1oinvd  7312  mapen  9179  mapfien  9445  hashfacen  14489  setcinv  18143  catcisolem  18163  symggrp  19432  f1omvdco2  19480  rngcinv  20653  ringcinv  20687  pf1mpf  22371  ufldom  23985  motgrp  28565  fmptco1f1o  32649  fcobij  32739  symgfcoeu  33084  pmtrcnel2  33092  cycpmconjslem1  33156  cycpmconjslem2  33157  reprpmtf1o  34619  subfacp1lem5  35168  ltrncoidN  40110  trlcoabs2N  40704  trlcoat  40705  trlcone  40710  cdlemg47  40718  tgrpgrplem  40731  tendoipl  40779  cdlemi2  40801  cdlemk2  40814  cdlemk4  40816  cdlemk8  40820  tendocnv  41003  dvhgrp  41089  cdlemn8  41186  dihopelvalcpre  41230  aks6d1c6lem5  42158  dssmap2d  44011  rngcinvALTV  48119  ringcinvALTV  48153