![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1ococnv1 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
f1ococnv1 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1orel 6835 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹) | |
2 | dfrel2 6187 | . . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹) | |
3 | 1, 2 | sylib 217 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡◡𝐹 = 𝐹) |
4 | 3 | coeq2d 5861 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = (◡𝐹 ∘ 𝐹)) |
5 | f1ocnv 6844 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
6 | f1ococnv2 6859 | . . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴)) | |
7 | 5, 6 | syl 17 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ ◡◡𝐹) = ( I ↾ 𝐴)) |
8 | 4, 7 | eqtr3d 2772 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 I cid 5572 ◡ccnv 5674 ↾ cres 5677 ∘ ccom 5679 Rel wrel 5680 –1-1-onto→wf1o 6541 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 |
This theorem is referenced by: f1cocnv1 6862 f1ocnvfv1 7276 fcof1oinvd 7293 mapen 9143 mapfien 9405 hashfacen 14417 hashfacenOLD 14418 setcinv 18044 catcisolem 18064 symggrp 19309 f1omvdco2 19357 pf1mpf 22091 ufldom 23686 motgrp 28061 fmptco1f1o 32124 fcobij 32214 symgfcoeu 32513 pmtrcnel2 32521 cycpmconjslem1 32583 cycpmconjslem2 32584 reprpmtf1o 33936 subfacp1lem5 34473 ltrncoidN 39302 trlcoabs2N 39896 trlcoat 39897 trlcone 39902 cdlemg47 39910 tgrpgrplem 39923 tendoipl 39971 cdlemi2 39993 cdlemk2 40006 cdlemk4 40008 cdlemk8 40012 tendocnv 40195 dvhgrp 40281 cdlemn8 40378 dihopelvalcpre 40422 dssmap2d 43075 rngcinv 46967 rngcinvALTV 46979 ringcinv 47018 ringcinvALTV 47042 |
Copyright terms: Public domain | W3C validator |