f1ococnv1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1ococnv1		Structured version Visualization version GIF version

Theorem f1ococnv1 6792

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 6766	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6136	. . . 4 ⊢ (Rel 𝐹 ↔ ^◡^◡𝐹 = 𝐹)
3	1, 2	sylib 218	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡^◡𝐹 = 𝐹)
4	3	coeq2d 5802	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = (^◡𝐹 ∘ 𝐹))
5		f1ocnv 6775	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6790	. . 3 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → (^◡𝐹 ∘ ^◡^◡𝐹) = ( I ↾ 𝐴))
7	5, 6	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = ( I ↾ 𝐴))
8	4, 7	eqtr3d 2768	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 I cid 5510 ^◡ccnv 5615 ↾ cres 5618 ∘ ccom 5620 Rel wrel 5621 –1-1-onto→wf1o 6480

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703 ax-sep 5234 ax-nul 5244 ax-pr 5370

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-sn 4577 df-pr 4579 df-op 4583 df-br 5092 df-opab 5154 df-id 5511 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488

This theorem is referenced by: f1cocnv1 6793 f1ocnvfv1 7210 fcof1oinvd 7227 mapen 9054 mapfien 9292 hashfacen 14361 setcinv 17997 catcisolem 18017 symggrp 19313 f1omvdco2 19361 rngcinv 20553 ringcinv 20587 pf1mpf 22268 ufldom 23878 motgrp 28522 fmptco1f1o 32613 fcobij 32701 cocnvf1o 32710 symgfcoeu 33049 pmtrcnel2 33057 cycpmconjslem1 33121 cycpmconjslem2 33122 reprpmtf1o 34637 subfacp1lem5 35226 ltrncoidN 40173 trlcoabs2N 40767 trlcoat 40768 trlcone 40773 cdlemg47 40781 tgrpgrplem 40794 tendoipl 40842 cdlemi2 40864 cdlemk2 40877 cdlemk4 40879 cdlemk8 40883 tendocnv 41066 dvhgrp 41152 cdlemn8 41249 dihopelvalcpre 41293 aks6d1c6lem5 42216 dssmap2d 44061 rngcinvALTV 48313 ringcinvALTV 48347

W3C validator