![]() |
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 6685 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
2 | cnvresid 6633 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
3 | 2 | fneq1i 6652 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
4 | 1, 3 | mpbir 230 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
5 | dff1o4 6846 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
6 | 1, 4, 5 | mpbir2an 709 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Colors of variables: wff setvar class |
Syntax hints: I cid 5575 ◡ccnv 5677 ↾ cres 5680 Fn wfn 6544 –1-1-onto→wf1o 6548 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 |
This theorem is referenced by: f1ovi 6877 fveqf1o 7311 f1ofvswap 7314 isoid 7336 enrefg 9005 ssdomg 9021 enreffi 9211 ssdomfi 9224 ssdomfi2 9225 wdomref 9597 infxpenc 10043 pwfseqlem5 10688 fproddvdsd 16315 wunndx 17167 idfucl 17870 idffth 17925 ressffth 17930 setccatid 18076 estrccatid 18125 funcestrcsetclem7 18140 funcestrcsetclem8 18141 equivestrcsetc 18146 funcsetcestrclem7 18155 funcsetcestrclem8 18156 idmgmhm 18664 idmhm 18755 ielefmnd 18847 sursubmefmnd 18856 injsubmefmnd 18857 idghm 19194 idresperm 19352 islinds2 21764 lindfres 21774 lindsmm 21779 mdetunilem9 22566 ssidcn 23203 resthauslem 23311 sshauslem 23320 idqtop 23654 fmid 23908 iducn 24232 mbfid 25608 dvid 25891 dvexp 25929 wilthlem2 27046 wilthlem3 27047 idmot 28413 ausgrusgrb 29050 upgrres1 29198 umgrres1 29199 usgrres1 29200 usgrexilem 29325 sizusglecusglem1 29347 pliguhgr 30368 hoif 31636 idunop 31860 idcnop 31863 elunop2 31895 fcobijfs 32587 symgcom 32896 fzo0pmtrlast 32905 pmtridf1o 32907 cycpmfvlem 32925 cycpmfv3 32928 cycpmcl 32929 islinds5 33178 ellspds 33179 qqhre 33752 rrhre 33753 subfacp1lem4 34924 subfacp1lem5 34925 poimirlem15 37239 poimirlem22 37246 idlaut 39699 tendoidcl 40372 tendo0co2 40391 erng1r 40598 dvalveclem 40628 dva0g 40630 dvh0g 40714 mzpresrename 42312 eldioph2lem1 42322 eldioph2lem2 42323 diophren 42375 kelac2 42631 lnrfg 42685 fundcmpsurbijinjpreimafv 46884 fundcmpsurinjimaid 46888 grimidvtxedg 47360 ushggricedg 47379 uspgrsprfo 47396 funcringcsetcALTV2lem8 47545 funcringcsetclem8ALTV 47568 itcovalendof 47928 |
Copyright terms: Public domain | W3C validator |