Theorem ex-pss

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

	Ref	Expression
Assertion	ex-pss	$$⊢\left\{1,2\right\}\subset \left\{1,2,3\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ex-ss	$$⊢\left\{1,2\right\}\subseteq \left\{1,2,3\right\}$$
2		3ex	$$⊢3\in \mathrm{V}$$
3	2	tpid3	$$⊢3\in \left\{1,2,3\right\}$$
4		1re	$$⊢1\in ℝ$$
5		1lt3	$$⊢1<3$$
6	4 5	gtneii	$$⊢3\ne 1$$
7		2re	$$⊢2\in ℝ$$
8		2lt3	$$⊢2<3$$
9	7 8	gtneii	$$⊢3\ne 2$$
10	6 9	nelpri	$$⊢\neg 3\in \left\{1,2\right\}$$
11		nelne1	$$⊢\left(3\in \left\{1,2,3\right\}\wedge \neg 3\in \left\{1,2\right\}\right)\to \left\{1,2,3\right\}\ne \left\{1,2\right\}$$
12	3 10 11	mp2an	$$⊢\left\{1,2,3\right\}\ne \left\{1,2\right\}$$
13	12	necomi	$$⊢\left\{1,2\right\}\ne \left\{1,2,3\right\}$$
14		df-pss	$$⊢\left\{1,2\right\}\subset \left\{1,2,3\right\}\leftrightarrow \left(\left\{1,2\right\}\subseteq \left\{1,2,3\right\}\wedge \left\{1,2\right\}\ne \left\{1,2,3\right\}\right)$$
15	1 13 14	mpbir2an	$$⊢\left\{1,2\right\}\subset \left\{1,2,3\right\}$$