![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relres | Structured version Visualization version GIF version |
Description: A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
relres | ⊢ Rel (𝐴 ↾ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res 5367 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss2 4054 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
3 | 1, 2 | eqsstri 3854 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
4 | relxp 5373 | . 2 ⊢ Rel (𝐵 × V) | |
5 | relss 5454 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3398 ∩ cin 3791 ⊆ wss 3792 × cxp 5353 ↾ cres 5357 Rel wrel 5360 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-in 3799 df-ss 3806 df-opab 4949 df-xp 5361 df-rel 5362 df-res 5367 |
This theorem is referenced by: elresOLD 5685 iss 5697 dfres2 5703 restidsing 5714 idrefOLD 5764 asymref 5767 poirr2 5775 cnvcnvres 5852 resco 5893 coeq0 5898 ressn 5925 funssres 6178 fnresdisj 6247 fnres 6253 fresaunres2 6326 fcnvres 6332 nfunsn 6484 dffv2 6531 fsnunfv 6724 resfunexgALT 7408 domss2 8407 fidomdm 8531 dmct 9681 relexp0rel 14184 setsres 16297 pospo 17359 metustid 22767 ovoliunlem1 23706 dvres 24112 dvres2 24113 dvlog 24834 efopnlem2 24840 h2hlm 28409 hlimcaui 28665 funresdm1 29979 dfpo2 32239 eqfunresadj 32252 dfrdg2 32289 funpartfun 32639 brres2 34669 elecres 34676 br1cnvssrres 34885 mapfzcons1 38244 diophrw 38286 eldioph2lem1 38287 eldioph2lem2 38288 undmrnresiss 38871 rtrclexi 38889 brfvrcld2 38945 relexpiidm 38957 rp-imass 39025 idhe 39041 limsupresuz 40847 liminfresuz 40928 funressnfv 42111 dfdfat2 42173 setrec2lem2 43550 |
Copyright terms: Public domain | W3C validator |