| 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 5672 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
| 2 | inss2 4189 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
| 3 | 1, 2 | eqsstri 3982 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
| 4 | relxp 5678 | . 2 ⊢ Rel (𝐵 × V) | |
| 5 | relss 5767 | . 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 3454 ∩ cin 3903 ⊆ wss 3904 × cxp 5658 ↾ cres 5662 Rel wrel 5665 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-ext 2734 |
| This proof depends on definitions: df-bi 210 df-an 401 df-tru 1572 df-ex 1809 df-sb 2096 df-clab 2741 df-cleq 2754 df-clel 2837 df-rab 3416 df-v 3456 df-in 3911 df-ss 3921 df-opab 5173 df-xp 5666 df-rel 5667 df-res 5672 |
| This theorem is used by: resindm 6028 relresdm1 6034 iss 6036 dfres2 6042 restidsing 6054 asymref 6115 poirr2 6123 cnvcnvres 6205 resco 6250 coeq0 6256 resssxp 6271 ressn 6286 dfpo2 6297 snres0 6299 funssres 6580 fnresdisj 6655 fnres 6662 fresaunres2 6750 fcnvres 6755 nfunsn 6920 dffv2 6976 fsnunfv 7185 eqfunresadj 7360 resfunexgALT 7943 elecres 8741 domss2 9122 fidomdm 9289 ttrclco 9685 cottrcl 9686 dmttrcl 9688 rnttrcl 9689 frmin 9719 frrlem16 9728 frr1 9729 dmct 10514 relexp0rel 15081 setsres 17244 pospo 18405 metustid 24722 ovoliunlem1 25672 dvres 26081 dvres2 26082 dvlog 26827 efopnlem2 26833 noetasuplem2 27909 noetainflem2 27913 h2hlm 31343 hlimcaui 31599 dfrdg2 36293 funpartfun 36443 bj-idreseq 37834 bj-idreseqb 37835 brres2 38950 br1cnvssrres 39262 refrelressn 39281 trrelressn 39344 dfeldisj2 39487 dfeldisj3 39488 dfeldisj4 39489 disjres 39521 antisymrelres 39543 antisymrelressn 39544 mapfzcons1 43476 diophrw 43518 eldioph2lem1 43519 eldioph2lem2 43520 undmrnresiss 44358 brfvrcld2 44446 relexpiidm 44458 limsupresuz 46445 liminfresuz 46526 funressnfv 47808 dfdfat2 47893 resinsn 49678 resinsnALT 49679 tposres0 49683 setrec2lem2 50500 |
| Copyright terms: Public domain | W3C validator |