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 6793

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 6767	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6138	. . . 4 ⊢ (Rel 𝐹 ↔ ^◡^◡𝐹 = 𝐹)
3	1, 2	sylib 218	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡^◡𝐹 = 𝐹)
4	3	coeq2d 5805	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = (^◡𝐹 ∘ 𝐹))
5		f1ocnv 6776	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6791	. . 3 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → (^◡𝐹 ∘ ^◡^◡𝐹) = ( I ↾ 𝐴))
7	5, 6	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = ( I ↾ 𝐴))
8	4, 7	eqtr3d 2766	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 I cid 5513 ^◡ccnv 5618 ↾ cres 5621 ∘ ccom 5623 Rel wrel 5624 –1-1-onto→wf1o 6481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5235 ax-nul 5245 ax-pr 5371

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ral 3045 df-rex 3054 df-rab 3395 df-v 3438 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-br 5093 df-opab 5155 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489

This theorem is referenced by: f1cocnv1 6794 f1ocnvfv1 7213 fcof1oinvd 7230 mapen 9058 mapfien 9298 hashfacen 14361 setcinv 17997 catcisolem 18017 symggrp 19279 f1omvdco2 19327 rngcinv 20522 ringcinv 20556 pf1mpf 22237 ufldom 23847 motgrp 28492 fmptco1f1o 32584 fcobij 32672 cocnvf1o 32681 symgfcoeu 33033 pmtrcnel2 33041 cycpmconjslem1 33105 cycpmconjslem2 33106 reprpmtf1o 34610 subfacp1lem5 35177 ltrncoidN 40127 trlcoabs2N 40721 trlcoat 40722 trlcone 40727 cdlemg47 40735 tgrpgrplem 40748 tendoipl 40796 cdlemi2 40818 cdlemk2 40831 cdlemk4 40833 cdlemk8 40837 tendocnv 41020 dvhgrp 41106 cdlemn8 41203 dihopelvalcpre 41247 aks6d1c6lem5 42170 dssmap2d 44015 rngcinvALTV 48280 ringcinvALTV 48314

W3C validator