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 6803

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 6777	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)
2		dfrel2 6147	. . . 4 ⊢ (Rel 𝐹 ↔ ^◡^◡𝐹 = 𝐹)
3	1, 2	sylib 218	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡^◡𝐹 = 𝐹)
4	3	coeq2d 5811	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (^◡𝐹 ∘ ^◡^◡𝐹) = (^◡𝐹 ∘ 𝐹))
5		f1ocnv 6786	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1-onto→𝐴)
6		f1ococnv2 6801	. . 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 5518 ^◡ccnv 5623 ↾ cres 5626 ∘ ccom 5628 Rel wrel 5629 –1-1-onto→wf1o 6491

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 2115 ax-9 2123 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

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 2715 df-cleq 2728 df-clel 2811 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499

This theorem is referenced by: f1cocnv1 6804 f1ocnvfv1 7222 fcof1oinvd 7239 mapen 9069 mapfien 9311 hashfacen 14377 setcinv 18014 catcisolem 18034 symggrp 19329 f1omvdco2 19377 rngcinv 20570 ringcinv 20604 pf1mpf 22296 ufldom 23906 motgrp 28615 fmptco1f1o 32711 fcobij 32799 cocnvf1o 32808 symgfcoeu 33164 pmtrcnel2 33172 cycpmconjslem1 33236 cycpmconjslem2 33237 reprpmtf1o 34783 subfacp1lem5 35378 ltrncoidN 40388 trlcoabs2N 40982 trlcoat 40983 trlcone 40988 cdlemg47 40996 tgrpgrplem 41009 tendoipl 41057 cdlemi2 41079 cdlemk2 41092 cdlemk4 41094 cdlemk8 41098 tendocnv 41281 dvhgrp 41367 cdlemn8 41464 dihopelvalcpre 41508 aks6d1c6lem5 42431 dssmap2d 44263 rngcinvALTV 48522 ringcinvALTV 48556

W3C validator