![]() |
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 6046 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
2 | cnvresid 6006 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
3 | 2 | fneq1i 6023 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
4 | 1, 3 | mpbir 221 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
5 | dff1o4 6183 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
6 | 1, 4, 5 | mpbir2an 975 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Colors of variables: wff setvar class |
Syntax hints: I cid 5052 ◡ccnv 5142 ↾ cres 5145 Fn wfn 5921 –1-1-onto→wf1o 5925 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 |
This theorem is referenced by: f1ovi 6213 fveqf1o 6597 isoid 6619 enrefg 8029 ssdomg 8043 hartogslem1 8488 wdomref 8518 infxpenc 8879 pwfseqlem5 9523 dfle2 12018 fproddvdsd 15106 wunndx 15925 idfucl 16588 idffth 16640 ressffth 16645 setccatid 16781 estrccatid 16819 funcestrcsetclem7 16833 funcestrcsetclem8 16834 equivestrcsetc 16839 funcsetcestrclem7 16848 funcsetcestrclem8 16849 idmhm 17391 idghm 17722 symggrp 17866 symgid 17867 idresperm 17875 islinds2 20200 lindfres 20210 lindsmm 20215 mdetunilem9 20474 ssidcn 21107 resthauslem 21215 sshauslem 21224 hausdiag 21496 idqtop 21557 fmid 21811 iducn 22134 mbfid 23448 dvid 23726 dvexp 23761 wilthlem2 24840 wilthlem3 24841 idmot 25477 ausgrusgrb 26105 upgrres1 26250 umgrres1 26251 usgrres1 26252 usgrexilem 26392 sizusglecusglem1 26413 pliguhgr 27468 hoif 28741 idunop 28965 idcnop 28968 elunop2 29000 fcobijfs 29629 pmtridf1o 29984 qqhre 30192 rrhre 30193 subfacp1lem4 31291 subfacp1lem5 31292 poimirlem15 33554 poimirlem22 33561 idlaut 35700 tendoidcl 36374 tendo0co2 36393 erng1r 36600 dvalveclem 36631 dva0g 36633 dvh0g 36717 mzpresrename 37630 eldioph2lem1 37640 eldioph2lem2 37641 diophren 37694 kelac2 37952 lnrfg 38006 uspgrsprfo 42081 idmgmhm 42113 funcringcsetcALTV2lem8 42368 funcringcsetclem8ALTV 42391 |
Copyright terms: Public domain | W3C validator |