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 5560 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss2 4203 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
3 | 1, 2 | eqsstri 3998 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
4 | relxp 5566 | . 2 ⊢ Rel (𝐵 × V) | |
5 | relss 5649 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3492 ∩ cin 3932 ⊆ wss 3933 × cxp 5546 ↾ cres 5550 Rel wrel 5553 |
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 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-in 3940 df-ss 3949 df-opab 5120 df-xp 5554 df-rel 5555 df-res 5560 |
This theorem is referenced by: iss 5896 dfres2 5902 restidsing 5915 asymref 5969 poirr2 5977 cnvcnvres 6055 resco 6096 coeq0 6101 ressn 6129 funssres 6391 fnresdisj 6460 fnres 6467 fresaunres2 6543 fcnvres 6549 nfunsn 6700 dffv2 6749 fsnunfv 6941 resfunexgALT 7638 domss2 8664 fidomdm 8789 dmct 9934 relexp0rel 14384 setsres 16513 pospo 17571 metustid 23091 ovoliunlem1 24030 dvres 24436 dvres2 24437 dvlog 25161 efopnlem2 25167 h2hlm 28684 hlimcaui 28940 funresdm1 30283 dfpo2 32888 eqfunresadj 32901 dfrdg2 32937 funpartfun 33301 bj-idreseq 34346 bj-idreseqb 34347 brres2 35410 elecres 35415 br1cnvssrres 35625 dfeldisj2 35831 dfeldisj3 35832 dfeldisj4 35833 mapfzcons1 39192 diophrw 39234 eldioph2lem1 39235 eldioph2lem2 39236 undmrnresiss 39842 brfvrcld2 39915 relexpiidm 39927 rp-imass 39995 limsupresuz 41860 liminfresuz 41941 funressnfv 43155 dfdfat2 43204 setrec2lem2 44725 |
Copyright terms: Public domain | W3C validator |