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 5597 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss2 4165 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
3 | 1, 2 | eqsstri 3956 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
4 | relxp 5603 | . 2 ⊢ Rel (𝐵 × V) | |
5 | relss 5687 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3427 ∩ cin 3887 ⊆ wss 3888 × cxp 5583 ↾ cres 5587 Rel wrel 5590 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1542 df-ex 1784 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3071 df-v 3429 df-in 3895 df-ss 3905 df-opab 5138 df-xp 5591 df-rel 5592 df-res 5597 |
This theorem is referenced by: iss 5937 dfres2 5943 restidsing 5956 asymref 6015 poirr2 6023 cnvcnvres 6102 resco 6148 coeq0 6153 resssxp 6167 ressn 6182 dfpo2 6193 funssres 6467 fnresdisj 6541 fnres 6548 fresaunres2 6635 fcnvres 6640 nfunsn 6798 dffv2 6850 fsnunfv 7046 resfunexgALT 7769 domss2 8877 fidomdm 9042 dmct 10227 relexp0rel 14692 setsres 16823 pospo 18007 metustid 23654 ovoliunlem1 24609 dvres 25018 dvres2 25019 dvlog 25749 efopnlem2 25755 h2hlm 29283 hlimcaui 29539 funresdm1 30885 snres0 33619 eqfunresadj 33683 dfrdg2 33719 ttrclco 33746 cottrcl 33747 dmttrcl 33749 rnttrcl 33750 noetasuplem2 33906 noetainflem2 33910 funpartfun 34214 bj-idreseq 35302 bj-idreseqb 35303 brres2 36376 elecres 36381 br1cnvssrres 36592 dfeldisj2 36798 dfeldisj3 36799 dfeldisj4 36800 mapfzcons1 40497 diophrw 40539 eldioph2lem1 40540 eldioph2lem2 40541 undmrnresiss 41143 brfvrcld2 41231 relexpiidm 41243 limsupresuz 43176 liminfresuz 43257 funressnfv 44466 dfdfat2 44549 setrec2lem2 46330 |
Copyright terms: Public domain | W3C validator |