Theorem nosgnn0

Description: (/) is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011)

	Ref	Expression
Assertion	nosgnn0	$$⊢\neg \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2	1	nesymi	$$⊢\neg \varnothing =1_{𝑜}$$
3		nsuceq0	$$⊢\mathrm{suc}{1}_{𝑜}\ne \varnothing$$
4		necom	$$⊢\mathrm{suc}{1}_{𝑜}\ne \varnothing \leftrightarrow \varnothing \ne \mathrm{suc}{1}_{𝑜}$$
5		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
6	5	neeq2i	$$⊢\varnothing \ne 2_{𝑜}\leftrightarrow \varnothing \ne \mathrm{suc}{1}_{𝑜}$$
7	4 6	bitr4i	$$⊢\mathrm{suc}{1}_{𝑜}\ne \varnothing \leftrightarrow \varnothing \ne 2_{𝑜}$$
8	3 7	mpbi	$$⊢\varnothing \ne 2_{𝑜}$$
9	8	neii	$$⊢\neg \varnothing =2_{𝑜}$$
10	2 9	pm3.2ni	$$⊢\neg \left(\varnothing =1_{𝑜}\vee \varnothing =2_{𝑜}\right)$$
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12	11	elpr	$$⊢\varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}\leftrightarrow \left(\varnothing =1_{𝑜}\vee \varnothing =2_{𝑜}\right)$$
13	10 12	mtbir	$$⊢\neg \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}$$