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 6469 | . 2 ⊢ ( I ↾ 𝐴) Fn 𝐴 | |
2 | cnvresid 6426 | . . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴) | |
3 | 2 | fneq1i 6443 | . . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴) |
4 | 1, 3 | mpbir 232 | . 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴 |
5 | dff1o4 6616 | . 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴)) | |
6 | 1, 4, 5 | mpbir2an 707 | 1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 |
Colors of variables: wff setvar class |
Syntax hints: I cid 5452 ◡ccnv 5547 ↾ cres 5550 Fn wfn 6343 –1-1-onto→wf1o 6347 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 |
This theorem is referenced by: f1ovi 6646 fveqf1o 7049 isoid 7071 enrefg 8529 ssdomg 8543 wdomref 9024 infxpenc 9432 pwfseqlem5 10073 fproddvdsd 15672 wunndx 16492 idfucl 17139 idffth 17191 ressffth 17196 setccatid 17332 estrccatid 17370 funcestrcsetclem7 17384 funcestrcsetclem8 17385 equivestrcsetc 17390 funcsetcestrclem7 17399 funcsetcestrclem8 17400 idmhm 17953 idghm 18311 idresperm 18448 symgid 18459 islinds2 20885 lindfres 20895 lindsmm 20900 mdetunilem9 21157 ssidcn 21791 resthauslem 21899 sshauslem 21908 idqtop 22242 fmid 22496 iducn 22819 mbfid 24163 dvid 24442 dvexp 24477 wilthlem2 25573 wilthlem3 25574 idmot 26250 ausgrusgrb 26877 upgrres1 27022 umgrres1 27023 usgrres1 27024 usgrexilem 27149 sizusglecusglem1 27170 pliguhgr 28190 hoif 29458 idunop 29682 idcnop 29685 elunop2 29717 fcobijfs 30385 symgcom 30654 pmtridf1o 30663 cycpmfvlem 30681 cycpmfv3 30684 cycpmcl 30685 islinds5 30859 ellspds 30860 qqhre 31160 rrhre 31161 subfacp1lem4 32327 subfacp1lem5 32328 poimirlem15 34788 poimirlem22 34795 idlaut 37112 tendoidcl 37785 tendo0co2 37804 erng1r 38011 dvalveclem 38041 dva0g 38043 dvh0g 38127 mzpresrename 39225 eldioph2lem1 39235 eldioph2lem2 39236 diophren 39288 kelac2 39543 lnrfg 39597 fundcmpsurbijinjpreimafv 43444 fundcmpsurinjimaid 43448 isomgreqve 43867 ushrisomgr 43883 uspgrsprfo 43900 idmgmhm 43932 ielefmnd 43984 sursubmefmnd 43993 injsubmefmnd 43994 funcringcsetcALTV2lem8 44242 funcringcsetclem8ALTV 44265 |
Copyright terms: Public domain | W3C validator |