| 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 6697 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
| 2 | cnvresid 6645 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
| 3 | 2 | fneq1i 6665 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
| 4 | 1, 3 | mpbir 231 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
| 5 | dff1o4 6856 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
| 6 | 1, 4, 5 | mpbir2an 711 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: I cid 5577 ◡ccnv 5684 ↾ cres 5687 Fn wfn 6556 –1-1-onto→wf1o 6560 |
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 |
| This theorem is referenced by: f1ovi 6887 fveqf1o 7322 f1ofvswap 7326 isoid 7349 enrefg 9024 ssdomg 9040 enreffi 9223 ssdomfi 9236 ssdomfi2 9237 wdomref 9612 infxpenc 10058 pwfseqlem5 10703 fproddvdsd 16372 wunndx 17232 idfucl 17926 idffth 17980 ressffth 17985 setccatid 18129 estrccatid 18176 funcestrcsetclem7 18191 funcestrcsetclem8 18192 equivestrcsetc 18197 funcsetcestrclem7 18206 funcsetcestrclem8 18207 idmgmhm 18714 idmhm 18808 ielefmnd 18900 sursubmefmnd 18909 injsubmefmnd 18910 idghm 19249 idresperm 19403 islinds2 21833 lindfres 21843 lindsmm 21848 mdetunilem9 22626 ssidcn 23263 resthauslem 23371 sshauslem 23380 idqtop 23714 fmid 23968 iducn 24292 mbfid 25670 dvid 25953 dvexp 25991 wilthlem2 27112 wilthlem3 27113 idmot 28545 ausgrusgrb 29182 upgrres1 29330 umgrres1 29331 usgrres1 29332 usgrexilem 29457 sizusglecusglem1 29479 pliguhgr 30505 hoif 31773 idunop 31997 idcnop 32000 elunop2 32032 fcobijfs 32734 symgcom 33103 fzo0pmtrlast 33112 pmtridf1o 33114 cycpmfvlem 33132 cycpmfv3 33135 cycpmcl 33136 islinds5 33395 ellspds 33396 qqhre 34021 rrhre 34022 subfacp1lem4 35188 subfacp1lem5 35189 poimirlem15 37642 poimirlem22 37649 idlaut 40098 tendoidcl 40771 tendo0co2 40790 erng1r 40997 dvalveclem 41027 dva0g 41029 dvh0g 41113 mzpresrename 42761 eldioph2lem1 42771 eldioph2lem2 42772 diophren 42824 kelac2 43077 lnrfg 43131 fundcmpsurbijinjpreimafv 47394 fundcmpsurinjimaid 47398 grimidvtxedg 47876 ushggricedg 47896 stgrusgra 47926 grlicref 47972 gpgusgra 48012 uspgrsprfo 48064 funcringcsetcALTV2lem8 48213 funcringcsetclem8ALTV 48236 itcovalendof 48590 tposidf1o 48787 oduoppcciso 49170 |
| Copyright terms: Public domain | W3C validator |