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 5922 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
2 | cnvresid 5882 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
3 | 2 | fneq1i 5899 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
4 | 1, 3 | mpbir 220 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
5 | dff1o4 6058 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
6 | 1, 4, 5 | mpbir2an 957 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Colors of variables: wff setvar class |
Syntax hints: I cid 4948 ◡ccnv 5037 ↾ cres 5040 Fn wfn 5799 –1-1-onto→wf1o 5803 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 |
This theorem is referenced by: f1ovi 6087 fveqf1o 6457 isoid 6479 enrefg 7873 ssdomg 7887 hartogslem1 8330 wdomref 8360 infxpenc 8724 pwfseqlem5 9364 dfle2 11856 fproddvdsd 14897 wunndx 15711 idfucl 16364 idffth 16416 ressffth 16421 setccatid 16557 estrccatid 16595 funcestrcsetclem7 16609 funcestrcsetclem8 16610 equivestrcsetc 16615 funcsetcestrclem7 16624 funcsetcestrclem8 16625 idmhm 17167 idghm 17498 symggrp 17643 symgid 17644 idresperm 17652 islinds2 19971 lindfres 19981 lindsmm 19986 mdetunilem9 20245 ssidcn 20869 resthauslem 20977 sshauslem 20986 hausdiag 21258 idqtop 21319 fmid 21574 iducn 21897 mbfid 23209 dvid 23487 dvexp 23522 wilthlem2 24595 wilthlem3 24596 idmot 25232 ausisusgra 25884 cusgraexilem2 25996 sizeusglecusglem1 26012 hoif 27997 idunop 28221 idcnop 28224 elunop2 28256 fcobijfs 28889 qqhre 29392 rrhre 29393 subfacp1lem4 30419 subfacp1lem5 30420 poimirlem15 32594 poimirlem22 32601 idlaut 34400 tendoidcl 35075 tendo0co2 35094 erng1r 35301 dvalveclem 35332 dva0g 35334 dvh0g 35418 mzpresrename 36331 eldioph2lem1 36341 eldioph2lem2 36342 diophren 36395 kelac2 36653 lnrfg 36708 ausgrusgrb 40395 upgrres1 40532 umgrres1 40533 usgrres1 40534 usgrexi 40661 sizusglecusglem1 40677 idmgmhm 41578 funcringcsetcALTV2lem8 41835 funcringcsetclem8ALTV 41858 |
Copyright terms: Public domain | W3C validator |