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 6818

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 6792	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6146	. . . 4 ⊢ (Rel 𝐹 ↔ ^◡^◡𝐹 = 𝐹)
3	1, 2	sylib 217	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡^◡𝐹 = 𝐹)
4	3	coeq2d 5823	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = (^◡𝐹 ∘ 𝐹))
5		f1ocnv 6801	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6816	. . 3 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → (^◡𝐹 ∘ ^◡^◡𝐹) = ( I ↾ 𝐴))
7	5, 6	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = ( I ↾ 𝐴))
8	4, 7	eqtr3d 2773	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 I cid 5535 ^◡ccnv 5637 ↾ cres 5640 ∘ ccom 5642 Rel wrel 5643 –1-1-onto→wf1o 6500

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pr 5389

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3406 df-v 3448 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508

This theorem is referenced by: f1cocnv1 6819 f1ocnvfv1 7227 fcof1oinvd 7244 mapen 9092 mapfien 9353 hashfacen 14363 hashfacenOLD 14364 setcinv 17990 catcisolem 18010 symggrp 19196 f1omvdco2 19244 pf1mpf 21755 ufldom 23350 motgrp 27548 fmptco1f1o 31614 fcobij 31707 symgfcoeu 32003 pmtrcnel2 32011 cycpmconjslem1 32073 cycpmconjslem2 32074 reprpmtf1o 33328 subfacp1lem5 33865 ltrncoidN 38664 trlcoabs2N 39258 trlcoat 39259 trlcone 39264 cdlemg47 39272 tgrpgrplem 39285 tendoipl 39333 cdlemi2 39355 cdlemk2 39368 cdlemk4 39370 cdlemk8 39374 tendocnv 39557 dvhgrp 39643 cdlemn8 39740 dihopelvalcpre 39784 dssmap2d 42416 rngcinv 46399 rngcinvALTV 46411 ringcinv 46450 ringcinvALTV 46474

W3C validator