![]() |
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 5531 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
2 | inss2 4156 | . . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V) | |
3 | 1, 2 | eqsstri 3949 | . 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V) |
4 | relxp 5537 | . 2 ⊢ Rel (𝐵 × V) | |
5 | relss 5620 | . 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵))) | |
6 | 3, 4, 5 | mp2 9 | 1 ⊢ Rel (𝐴 ↾ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3441 ∩ cin 3880 ⊆ wss 3881 × cxp 5517 ↾ cres 5521 Rel wrel 5524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-in 3888 df-ss 3898 df-opab 5093 df-xp 5525 df-rel 5526 df-res 5531 |
This theorem is referenced by: iss 5870 dfres2 5876 restidsing 5889 asymref 5943 poirr2 5951 cnvcnvres 6029 resco 6070 coeq0 6075 resssxp 6089 ressn 6104 funssres 6368 fnresdisj 6439 fnres 6446 fresaunres2 6524 fcnvres 6530 nfunsn 6682 dffv2 6733 fsnunfv 6926 resfunexgALT 7631 domss2 8660 fidomdm 8785 dmct 9935 relexp0rel 14388 setsres 16517 pospo 17575 metustid 23161 ovoliunlem1 24106 dvres 24514 dvres2 24515 dvlog 25242 efopnlem2 25248 h2hlm 28763 hlimcaui 29019 funresdm1 30368 dfpo2 33104 eqfunresadj 33117 dfrdg2 33153 funpartfun 33517 bj-idreseq 34577 bj-idreseqb 34578 brres2 35689 elecres 35694 br1cnvssrres 35905 dfeldisj2 36111 dfeldisj3 36112 dfeldisj4 36113 mapfzcons1 39658 diophrw 39700 eldioph2lem1 39701 eldioph2lem2 39702 undmrnresiss 40304 brfvrcld2 40393 relexpiidm 40405 limsupresuz 42345 liminfresuz 42426 funressnfv 43635 dfdfat2 43684 setrec2lem2 45224 |
Copyright terms: Public domain | W3C validator |