![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1ococnv2 | Structured version Visualization version GIF version |
Description: The composition of a one-to-one onto function and its converse equals the identity relation restricted to the function's range. (Contributed by NM, 13-Dec-2003.) (Proof shortened by Stefan O'Rear, 12-Feb-2015.) |
Ref | Expression |
---|---|
f1ococnv2 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ofo 6493 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) | |
2 | fococnv2 6511 | . 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 I cid 5350 ◡ccnv 5445 ↾ cres 5448 ∘ ccom 5450 –onto→wfo 6226 –1-1-onto→wf1o 6227 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pr 5224 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-op 4481 df-br 4965 df-opab 5027 df-id 5351 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 |
This theorem is referenced by: f1ococnv1 6514 f1ocnvfv2 6902 mapen 8531 hashfacen 13660 setcinv 17179 catcisolem 17195 symginv 18261 f1omvdco2 18307 gsumval3 18748 gsumzf1o 18753 psrass1lem 19845 evl1var 20181 pf1ind 20200 fcobij 30138 symgfcoeu 30377 cycpmconjvlem 30412 cycpmconjs 30428 cyc3conja 30429 erdsze2lem2 32053 ltrncoidN 36808 cdlemg46 37415 cdlemk45 37627 cdlemk55a 37639 tendocnv 37701 eldioph2 38857 rngcinv 43744 rngcinvALTV 43756 ringcinv 43795 ringcinvALTV 43819 |
Copyright terms: Public domain | W3C validator |