Theorem f1ococnv1 6880

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-1onto𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

Proof of Theorem f1ococnv1

Step	Hyp	Ref	Expression
1		f1orel 6852	. . . 4 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → Rel 𝐹)
2		dfrel2 6194	. . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3	1, 2	sylib 221	. . 3 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡◡𝐹 = 𝐹)
4	3	coeq2d 5847	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → (◡𝐹 ∘ ◡◡𝐹) = (◡𝐹 ∘ 𝐹))
5		f1ocnv 6862	. . 3 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶1-1onto𝐴)
6		f1ococnv2 6878	. . 3 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴))
7	5, 6	syl 18	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴))
8	4, 7	eqtr3d 2800	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   I cid 5550  ^◡ccnv 5655   ↾ cres 5658   ∘ ccom 5660  Rel wrel 5661  ⟶1-1ontowf1o 6560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is used by:  f1cocnv1  6881  f1ocnvfv1  7310  fcof1oinvd  7327  mapen  9191  mapfien  9430  hashfacen  14629  setcinv  18297  catcisolem  18317  symggrp  19647  f1omvdco2  19695  rngcinv  20922  ringcinv  20956  pf1mpf  22703  ufldom  24314  motgrp  29039  fmptco1f1o  33302  fcobij  33385  cocnvf1o  33394  symgfcoeu  33719  pmtrcnel2  33727  cycpmconjslem1  33791  cycpmconjslem2  33792  reprpmtf1o  35338  subfacp1lem5  36129  ltrncoidN  41388  trlcoabs2N  41982  trlcoat  41983  trlcone  41988  cdlemg47  41996  tgrpgrplem  42009  tendoipl  42057  cdlemi2  42079  cdlemk2  42092  cdlemk4  42094  cdlemk8  42098  tendocnv  42281  dvhgrp  42367  cdlemn8  42464  dihopelvalcpre  42508  aks6d1c6lem5  43430  dssmap2d  45225  rngcinvALTV  49588  ringcinvALTV  49622