Theorem f1ococnv1 6646

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 6621	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6021	. . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3	1, 2	sylib 221	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡◡𝐹 = 𝐹)
4	3	coeq2d 5705	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = (◡𝐹 ∘ 𝐹))
5		f1ocnv 6630	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6644	. . 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 5428  ^◡ccnv 5524   ↾ cres 5527   ∘ ccom 5529  Rel wrel 5530  –1-1-onto→wf1o 6338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346

This theorem is referenced by:  f1cocnv1  6647  f1ocnvfv1  7044  fcof1oinvd  7060  mapen  8731  mapfien  8945  hashfacen  13904  hashfacenOLD  13905  setcinv  17462  catcisolem  17482  symggrp  18646  f1omvdco2  18694  pf1mpf  21122  ufldom  22713  motgrp  26489  fmptco1f1o  30542  fcobij  30632  symgfcoeu  30928  pmtrcnel2  30936  cycpmconjslem1  30998  cycpmconjslem2  30999  reprpmtf1o  32176  subfacp1lem5  32717  ltrncoidN  37765  trlcoabs2N  38359  trlcoat  38360  trlcone  38365  cdlemg47  38373  tgrpgrplem  38386  tendoipl  38434  cdlemi2  38456  cdlemk2  38469  cdlemk4  38471  cdlemk8  38475  tendocnv  38658  dvhgrp  38744  cdlemn8  38841  dihopelvalcpre  38885  dssmap2d  41176  rngcinv  45073  rngcinvALTV  45085  ringcinv  45124  ringcinvALTV  45148