# Metamath Proof Explorer

## Theorem ex-res

Description: Example for df-res . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-res ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {{F}↾}_{{B}}=\left\{⟨2,6⟩\right\}$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}$
2 df-pr ${⊢}\left\{⟨2,6⟩,⟨3,9⟩\right\}=\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}$
3 1 2 eqtrdi ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {F}=\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}$
4 3 reseq1d ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {{F}↾}_{{B}}={\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)↾}_{{B}}$
5 resundir ${⊢}{\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)↾}_{{B}}=\left({\left\{⟨2,6⟩\right\}↾}_{{B}}\right)\cup \left({\left\{⟨3,9⟩\right\}↾}_{{B}}\right)$
6 4 5 eqtrdi ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {{F}↾}_{{B}}=\left({\left\{⟨2,6⟩\right\}↾}_{{B}}\right)\cup \left({\left\{⟨3,9⟩\right\}↾}_{{B}}\right)$
7 2re ${⊢}2\in ℝ$
8 7 elexi ${⊢}2\in \mathrm{V}$
9 6re ${⊢}6\in ℝ$
10 9 elexi ${⊢}6\in \mathrm{V}$
11 8 10 relsnop ${⊢}\mathrm{Rel}\left\{⟨2,6⟩\right\}$
12 dmsnopss ${⊢}\mathrm{dom}\left\{⟨2,6⟩\right\}\subseteq \left\{2\right\}$
13 snsspr2 ${⊢}\left\{2\right\}\subseteq \left\{1,2\right\}$
14 simpr ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {B}=\left\{1,2\right\}$
15 13 14 sseqtrrid ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to \left\{2\right\}\subseteq {B}$
16 12 15 sstrid ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to \mathrm{dom}\left\{⟨2,6⟩\right\}\subseteq {B}$
17 relssres ${⊢}\left(\mathrm{Rel}\left\{⟨2,6⟩\right\}\wedge \mathrm{dom}\left\{⟨2,6⟩\right\}\subseteq {B}\right)\to {\left\{⟨2,6⟩\right\}↾}_{{B}}=\left\{⟨2,6⟩\right\}$
18 11 16 17 sylancr ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {\left\{⟨2,6⟩\right\}↾}_{{B}}=\left\{⟨2,6⟩\right\}$
19 1re ${⊢}1\in ℝ$
20 1lt3 ${⊢}1<3$
21 19 20 gtneii ${⊢}3\ne 1$
22 2lt3 ${⊢}2<3$
23 7 22 gtneii ${⊢}3\ne 2$
24 21 23 nelpri ${⊢}¬3\in \left\{1,2\right\}$
25 14 eleq2d ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to \left(3\in {B}↔3\in \left\{1,2\right\}\right)$
26 24 25 mtbiri ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to ¬3\in {B}$
27 ressnop0 ${⊢}¬3\in {B}\to {\left\{⟨3,9⟩\right\}↾}_{{B}}=\varnothing$
28 26 27 syl ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {\left\{⟨3,9⟩\right\}↾}_{{B}}=\varnothing$
29 18 28 uneq12d ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to \left({\left\{⟨2,6⟩\right\}↾}_{{B}}\right)\cup \left({\left\{⟨3,9⟩\right\}↾}_{{B}}\right)=\left\{⟨2,6⟩\right\}\cup \varnothing$
30 un0 ${⊢}\left\{⟨2,6⟩\right\}\cup \varnothing =\left\{⟨2,6⟩\right\}$
31 29 30 eqtrdi ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to \left({\left\{⟨2,6⟩\right\}↾}_{{B}}\right)\cup \left({\left\{⟨3,9⟩\right\}↾}_{{B}}\right)=\left\{⟨2,6⟩\right\}$
32 6 31 eqtrd ${⊢}\left({F}=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge {B}=\left\{1,2\right\}\right)\to {{F}↾}_{{B}}=\left\{⟨2,6⟩\right\}$