![]() |
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 5694 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss2 4231 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
3 | 1, 2 | eqsstri 4014 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
4 | relxp 5700 | . 2 ⊢ Rel (𝐵 × V) | |
5 | relss 5787 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3462 ∩ cin 3946 ⊆ wss 3947 × cxp 5680 ↾ cres 5684 Rel wrel 5687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-in 3954 df-ss 3964 df-opab 5216 df-xp 5688 df-rel 5689 df-res 5694 |
This theorem is referenced by: relresdm1 6042 iss 6044 dfres2 6050 restidsing 6062 asymref 6128 poirr2 6136 cnvcnvres 6216 resco 6261 coeq0 6266 resssxp 6281 ressn 6296 dfpo2 6307 snres0 6309 funssres 6603 fnresdisj 6681 fnres 6688 fresaunres2 6774 fcnvres 6779 nfunsn 6943 dffv2 6997 fsnunfv 7201 eqfunresadj 7372 resfunexgALT 7961 domss2 9174 fidomdm 9376 ttrclco 9761 cottrcl 9762 dmttrcl 9764 rnttrcl 9765 frmin 9792 frrlem16 9801 frr1 9802 dmct 10567 relexp0rel 15042 setsres 17180 pospo 18370 metustid 24554 ovoliunlem1 25522 dvres 25931 dvres2 25932 dvlog 26678 efopnlem2 26684 noetasuplem2 27764 noetainflem2 27768 h2hlm 30913 hlimcaui 31169 dfrdg2 35619 funpartfun 35767 bj-idreseq 36869 bj-idreseqb 36870 brres2 37966 elecres 37975 br1cnvssrres 38203 refrelressn 38222 trrelressn 38281 dfeldisj2 38416 dfeldisj3 38417 dfeldisj4 38418 disjres 38442 antisymrelres 38461 antisymrelressn 38462 mapfzcons1 42374 diophrw 42416 eldioph2lem1 42417 eldioph2lem2 42418 undmrnresiss 43271 brfvrcld2 43359 relexpiidm 43371 limsupresuz 45324 liminfresuz 45405 funressnfv 46658 dfdfat2 46741 setrec2lem2 48440 |
Copyright terms: Public domain | W3C validator |