Theorem nosgnn0i

Description: If X is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011)

	Ref	Expression
Hypothesis	nosgnn0i.1	$$⊢X\in \left\{1_{𝑜},2_{𝑜}\right\}$$
Assertion	nosgnn0i	$$⊢\varnothing \ne X$$

Proof

Step	Hyp	Ref	Expression
1		nosgnn0i.1	$$⊢X\in \left\{1_{𝑜},2_{𝑜}\right\}$$
2		nosgnn0	$$⊢\neg \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}$$
3		eleq1	$$⊢\varnothing =X\to \left(\varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}\leftrightarrow X\in \left\{1_{𝑜},2_{𝑜}\right\}\right)$$
4	1 3	mpbiri	$$⊢\varnothing =X\to \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}$$
5	2 4	mto	$$⊢\neg \varnothing =X$$
6	5	neir	$$⊢\varnothing \ne X$$