| 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 5675 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
| 2 | inss2 4190 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
| 3 | 1, 2 | eqsstri 3984 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
| 4 | relxp 5681 | . 2 ⊢ Rel (𝐵 × V) | |
| 5 | relss 5770 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
| 6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: Vcvv 3457 ∩ cin 3905 ⊆ wss 3906 × cxp 5661 ↾ cres 5665 Rel wrel 5668 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 |
| This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3419 df-v 3459 df-in 3913 df-ss 3923 df-opab 5176 df-xp 5669 df-rel 5670 df-res 5675 |
| This theorem is used by: resindm 6031 relresdm1 6037 iss 6039 dfres2 6045 restidsing 6057 asymref 6118 poirr2 6126 cnvcnvres 6208 resco 6253 coeq0 6259 resssxp 6274 ressn 6290 dfpo2 6301 snres0 6303 funssres 6584 fnresdisj 6659 fnres 6666 fresaunres2 6754 fcnvres 6759 nfunsn 6924 dffv2 6980 fsnunfv 7191 eqfunresadj 7369 resfunexgALT 7951 elecres 8749 domss2 9131 fidomdm 9298 ttrclco 9694 cottrcl 9695 dmttrcl 9697 rnttrcl 9698 frmin 9728 frrlem16 9737 frr1 9738 dmct 10523 relexp0rel 15100 setsres 17262 pospo 18423 metustid 24764 ovoliunlem1 25714 dvres 26123 dvres2 26124 dvlog 26869 efopnlem2 26875 noetasuplem2 27951 noetainflem2 27955 h2hlm 31405 hlimcaui 31661 dfrdg2 36324 funpartfun 36474 bj-idreseq 37865 bj-idreseqb 37866 brres2 38982 br1cnvssrres 39294 refrelressn 39313 trrelressn 39376 dfeldisj2 39519 dfeldisj3 39520 dfeldisj4 39521 disjres 39553 antisymrelres 39575 antisymrelressn 39576 mapfzcons1 43508 diophrw 43550 eldioph2lem1 43551 eldioph2lem2 43552 undmrnresiss 44390 brfvrcld2 44478 relexpiidm 44490 limsupresuz 46477 liminfresuz 46558 funressnfv 47840 dfdfat2 47925 resinsn 49709 resinsnALT 49710 tposres0 49714 setrec2lem2 50531 |
| Copyright terms: Public domain | W3C validator |