![]() |
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 6634 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
2 | cnvresid 6584 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
3 | 2 | fneq1i 6603 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
4 | 1, 3 | mpbir 230 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
5 | dff1o4 6796 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
6 | 1, 4, 5 | mpbir2an 710 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Colors of variables: wff setvar class |
Syntax hints: I cid 5534 ◡ccnv 5636 ↾ cres 5639 Fn wfn 6495 –1-1-onto→wf1o 6499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-br 5110 df-opab 5172 df-id 5535 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 |
This theorem is referenced by: f1ovi 6827 fveqf1o 7253 f1ofvswap 7256 isoid 7278 enrefg 8930 ssdomg 8946 enreffi 9136 ssdomfi 9149 ssdomfi2 9150 wdomref 9516 infxpenc 9962 pwfseqlem5 10607 fproddvdsd 16225 wunndx 17075 idfucl 17775 idffth 17828 ressffth 17833 setccatid 17978 estrccatid 18027 funcestrcsetclem7 18042 funcestrcsetclem8 18043 equivestrcsetc 18048 funcsetcestrclem7 18057 funcsetcestrclem8 18058 idmhm 18619 ielefmnd 18705 sursubmefmnd 18714 injsubmefmnd 18715 idghm 19031 idresperm 19175 islinds2 21242 lindfres 21252 lindsmm 21257 mdetunilem9 21992 ssidcn 22629 resthauslem 22737 sshauslem 22746 idqtop 23080 fmid 23334 iducn 23658 mbfid 25022 dvid 25305 dvexp 25340 wilthlem2 26441 wilthlem3 26442 idmot 27528 ausgrusgrb 28165 upgrres1 28310 umgrres1 28311 usgrres1 28312 usgrexilem 28437 sizusglecusglem1 28458 pliguhgr 29477 hoif 30745 idunop 30969 idcnop 30972 elunop2 31004 fcobijfs 31694 symgcom 31990 pmtridf1o 31999 cycpmfvlem 32017 cycpmfv3 32020 cycpmcl 32021 islinds5 32210 ellspds 32211 qqhre 32665 rrhre 32666 subfacp1lem4 33841 subfacp1lem5 33842 poimirlem15 36143 poimirlem22 36150 idlaut 38609 tendoidcl 39282 tendo0co2 39301 erng1r 39508 dvalveclem 39538 dva0g 39540 dvh0g 39624 mzpresrename 41120 eldioph2lem1 41130 eldioph2lem2 41131 diophren 41183 kelac2 41439 lnrfg 41493 fundcmpsurbijinjpreimafv 45689 fundcmpsurinjimaid 45693 isomgreqve 46107 ushrisomgr 46123 uspgrsprfo 46140 idmgmhm 46172 funcringcsetcALTV2lem8 46431 funcringcsetclem8ALTV 46454 itcovalendof 46845 |
Copyright terms: Public domain | W3C validator |