![]() |
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 5689 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss2 4230 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
3 | 1, 2 | eqsstri 4017 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
4 | relxp 5695 | . 2 ⊢ Rel (𝐵 × V) | |
5 | relss 5782 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3475 ∩ cin 3948 ⊆ wss 3949 × cxp 5675 ↾ cres 5679 Rel wrel 5682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-in 3956 df-ss 3966 df-opab 5212 df-xp 5683 df-rel 5684 df-res 5689 |
This theorem is referenced by: relresdm1 6034 iss 6036 dfres2 6042 restidsing 6053 asymref 6118 poirr2 6126 cnvcnvres 6205 resco 6250 coeq0 6255 resssxp 6270 ressn 6285 dfpo2 6296 snres0 6298 funssres 6593 fnresdisj 6671 fnres 6678 fresaunres2 6764 fcnvres 6769 nfunsn 6934 dffv2 6987 fsnunfv 7185 eqfunresadj 7357 resfunexgALT 7934 domss2 9136 fidomdm 9329 ttrclco 9713 cottrcl 9714 dmttrcl 9716 rnttrcl 9717 frmin 9744 frrlem16 9753 frr1 9754 dmct 10519 relexp0rel 14984 setsres 17111 pospo 18298 metustid 24063 ovoliunlem1 25019 dvres 25428 dvres2 25429 dvlog 26159 efopnlem2 26165 noetasuplem2 27237 noetainflem2 27241 h2hlm 30233 hlimcaui 30489 dfrdg2 34767 funpartfun 34915 bj-idreseq 36043 bj-idreseqb 36044 brres2 37136 elecres 37145 br1cnvssrres 37375 refrelressn 37394 trrelressn 37453 dfeldisj2 37588 dfeldisj3 37589 dfeldisj4 37590 disjres 37614 antisymrelres 37633 antisymrelressn 37634 mapfzcons1 41455 diophrw 41497 eldioph2lem1 41498 eldioph2lem2 41499 undmrnresiss 42355 brfvrcld2 42443 relexpiidm 42455 limsupresuz 44419 liminfresuz 44500 funressnfv 45753 dfdfat2 45836 setrec2lem2 47739 |
Copyright terms: Public domain | W3C validator |