Theorem f1ococnv1 6863

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 6837	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6189	. . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3	1, 2	sylib 217	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡◡𝐹 = 𝐹)
4	3	coeq2d 5863	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = (◡𝐹 ∘ 𝐹))
5		f1ocnv 6846	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6861	. . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴))
7	5, 6	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴))
8	4, 7	eqtr3d 2775	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

Syntax hints:   → wi 4   = wceq 1542   I cid 5574  ^◡ccnv 5676   ↾ cres 5679   ∘ ccom 5681  Rel wrel 5682  –1-1-onto→wf1o 6543

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551

This theorem is referenced by:  f1cocnv1  6864  f1ocnvfv1  7274  fcof1oinvd  7291  mapen  9141  mapfien  9403  hashfacen  14413  hashfacenOLD  14414  setcinv  18040  catcisolem  18060  symggrp  19268  f1omvdco2  19316  pf1mpf  21871  ufldom  23466  motgrp  27794  fmptco1f1o  31857  fcobij  31947  symgfcoeu  32243  pmtrcnel2  32251  cycpmconjslem1  32313  cycpmconjslem2  32314  reprpmtf1o  33638  subfacp1lem5  34175  ltrncoidN  38999  trlcoabs2N  39593  trlcoat  39594  trlcone  39599  cdlemg47  39607  tgrpgrplem  39620  tendoipl  39668  cdlemi2  39690  cdlemk2  39703  cdlemk4  39705  cdlemk8  39709  tendocnv  39892  dvhgrp  39978  cdlemn8  40075  dihopelvalcpre  40119  dssmap2d  42773  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954