![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oi | Structured version Visualization version GIF version |
Description: A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
f1oi | ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnresi 6254 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
2 | cnvresid 6213 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
3 | 2 | fneq1i 6230 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
4 | 1, 3 | mpbir 223 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
5 | dff1o4 6399 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
6 | 1, 4, 5 | mpbir2an 701 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Colors of variables: wff setvar class |
Syntax hints: I cid 5260 ◡ccnv 5354 ↾ cres 5357 Fn wfn 6130 –1-1-onto→wf1o 6134 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-opab 4949 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 |
This theorem is referenced by: f1ovi 6429 fveqf1o 6829 isoid 6851 enrefg 8273 ssdomg 8287 wdomref 8766 infxpenc 9174 pwfseqlem5 9820 fproddvdsd 15463 wunndx 16276 idfucl 16926 idffth 16978 ressffth 16983 setccatid 17119 estrccatid 17157 funcestrcsetclem7 17172 funcestrcsetclem8 17173 equivestrcsetc 17178 funcsetcestrclem7 17187 funcsetcestrclem8 17188 idmhm 17730 idghm 18059 symggrp 18203 symgid 18204 idresperm 18212 islinds2 20556 lindfres 20566 lindsmm 20571 mdetunilem9 20831 ssidcn 21467 resthauslem 21575 sshauslem 21584 idqtop 21918 fmid 22172 iducn 22495 mbfid 23839 dvid 24118 dvexp 24153 wilthlem2 25247 wilthlem3 25248 idmot 25888 ausgrusgrb 26514 upgrres1 26660 umgrres1 26661 usgrres1 26662 usgrexilem 26788 sizusglecusglem1 26809 pliguhgr 27913 hoif 29185 idunop 29409 idcnop 29412 elunop2 29444 fcobijfs 30067 islinds5 30414 ellspds 30415 pmtridf1o 30454 qqhre 30662 rrhre 30663 subfacp1lem4 31764 subfacp1lem5 31765 poimirlem15 34050 poimirlem22 34057 idlaut 36250 tendoidcl 36923 tendo0co2 36942 erng1r 37149 dvalveclem 37179 dva0g 37181 dvh0g 37265 mzpresrename 38273 eldioph2lem1 38283 eldioph2lem2 38284 diophren 38337 kelac2 38594 lnrfg 38648 isomgreqve 42738 ushrisomgr 42754 uspgrsprfo 42771 idmgmhm 42803 funcringcsetcALTV2lem8 43058 funcringcsetclem8ALTV 43081 |
Copyright terms: Public domain | W3C validator |