Theorem f1ococnv1 6859

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 6833	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6185	. . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3	1, 2	sylib 217	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡◡𝐹 = 𝐹)
4	3	coeq2d 5860	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = (◡𝐹 ∘ 𝐹))
5		f1ocnv 6842	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6857	. . 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 5572  ^◡ccnv 5674   ↾ cres 5677   ∘ ccom 5679  Rel wrel 5680  –1-1-onto→wf1o 6539

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 5298  ax-nul 5305  ax-pr 5426

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 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is referenced by:  f1cocnv1  6860  f1ocnvfv1  7269  fcof1oinvd  7286  mapen  9137  mapfien  9399  hashfacen  14409  hashfacenOLD  14410  setcinv  18036  catcisolem  18056  symggrp  19261  f1omvdco2  19309  pf1mpf  21853  ufldom  23448  motgrp  27774  fmptco1f1o  31835  fcobij  31925  symgfcoeu  32221  pmtrcnel2  32229  cycpmconjslem1  32291  cycpmconjslem2  32292  reprpmtf1o  33576  subfacp1lem5  34113  ltrncoidN  38937  trlcoabs2N  39531  trlcoat  39532  trlcone  39537  cdlemg47  39545  tgrpgrplem  39558  tendoipl  39606  cdlemi2  39628  cdlemk2  39641  cdlemk4  39643  cdlemk8  39647  tendocnv  39830  dvhgrp  39916  cdlemn8  40013  dihopelvalcpre  40057  dssmap2d  42706  rngcinv  46781  rngcinvALTV  46793  ringcinv  46832  ringcinvALTV  46856