| 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 5697 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
| 2 | inss2 4238 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
| 3 | 1, 2 | eqsstri 4030 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
| 4 | relxp 5703 | . 2 ⊢ Rel (𝐵 × V) | |
| 5 | relss 5791 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
| 6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: Vcvv 3480 ∩ cin 3950 ⊆ wss 3951 × cxp 5683 ↾ cres 5687 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 df-res 5697 |
| This theorem is referenced by: relresdm1 6051 iss 6053 dfres2 6059 restidsing 6071 asymref 6136 poirr2 6144 cnvcnvres 6225 resco 6270 coeq0 6275 resssxp 6290 ressn 6305 dfpo2 6316 snres0 6318 funssres 6610 fnresdisj 6688 fnres 6695 fresaunres2 6780 fcnvres 6785 nfunsn 6948 dffv2 7004 fsnunfv 7207 eqfunresadj 7380 resfunexgALT 7972 domss2 9176 fidomdm 9374 ttrclco 9758 cottrcl 9759 dmttrcl 9761 rnttrcl 9762 frmin 9789 frrlem16 9798 frr1 9799 dmct 10564 relexp0rel 15076 setsres 17215 pospo 18390 metustid 24567 ovoliunlem1 25537 dvres 25946 dvres2 25947 dvlog 26693 efopnlem2 26699 noetasuplem2 27779 noetainflem2 27783 h2hlm 30999 hlimcaui 31255 dfrdg2 35796 funpartfun 35944 bj-idreseq 37163 bj-idreseqb 37164 brres2 38269 elecres 38278 br1cnvssrres 38506 refrelressn 38525 trrelressn 38584 dfeldisj2 38719 dfeldisj3 38720 dfeldisj4 38721 disjres 38745 antisymrelres 38764 antisymrelressn 38765 mapfzcons1 42728 diophrw 42770 eldioph2lem1 42771 eldioph2lem2 42772 undmrnresiss 43617 brfvrcld2 43705 relexpiidm 43717 limsupresuz 45718 liminfresuz 45799 funressnfv 47055 dfdfat2 47140 resinsn 48772 resinsnALT 48773 tposres0 48777 setrec2lem2 49213 |
| Copyright terms: Public domain | W3C validator |