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	⊢ 𝑋 ∈ { 1o , 2o }
Assertion	nosgnn0i	⊢ ∅ ≠ 𝑋

Proof

Step	Hyp	Ref	Expression
1		nosgnn0i.1	⊢ 𝑋 ∈ { 1o , 2o }
2		nosgnn0	⊢ ¬ ∅ ∈ { 1o , 2o }
3		eleq1	⊢ ( ∅ = 𝑋 → ( ∅ ∈ { 1o , 2o } ↔ 𝑋 ∈ { 1o , 2o } ) )
4	1 3	mpbiri	⊢ ( ∅ = 𝑋 → ∅ ∈ { 1o , 2o } )
5	2 4	mto	⊢ ¬ ∅ = 𝑋
6	5	neir	⊢ ∅ ≠ 𝑋