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\upharpoonright }_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	syl6eq	$$⊢\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\upharpoonright }_B={\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)\upharpoonright }_B$$
5		resundir	$$⊢{\left(\left\{⟨2,6⟩\right\}\cup \left\{⟨3,9⟩\right\}\right)\upharpoonright }_B=\left({\left\{⟨2,6⟩\right\}\upharpoonright }_B\right)\cup \left({\left\{⟨3,9⟩\right\}\upharpoonright }_B\right)$$
6	4 5	syl6eq	$$⊢\left(F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge B=\left\{1,2\right\}\right)\to {F\upharpoonright }_B=\left({\left\{⟨2,6⟩\right\}\upharpoonright }_B\right)\cup \left({\left\{⟨3,9⟩\right\}\upharpoonright }_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\}\upharpoonright }_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\}\upharpoonright }_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	$$⊢\neg 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\leftrightarrow 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 \neg 3\in B$$
27		ressnop0	$$⊢\neg 3\in B\to {\left\{⟨3,9⟩\right\}\upharpoonright }_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\}\upharpoonright }_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\}\upharpoonright }_B\right)\cup \left({\left\{⟨3,9⟩\right\}\upharpoonright }_B\right)=\left\{⟨2,6⟩\right\}\cup \varnothing$$
30		un0	$$⊢\left\{⟨2,6⟩\right\}\cup \varnothing =\left\{⟨2,6⟩\right\}$$
31	29 30	syl6eq	$$⊢\left(F=\left\{⟨2,6⟩,⟨3,9⟩\right\}\wedge B=\left\{1,2\right\}\right)\to \left({\left\{⟨2,6⟩\right\}\upharpoonright }_B\right)\cup \left({\left\{⟨3,9⟩\right\}\upharpoonright }_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\upharpoonright }_B=\left\{⟨2,6⟩\right\}$$