Theorem 0nsr

Description: The empty set is not a signed real. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	0nsr	$$⊢\neg \varnothing \in 𝑹$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		enrer	$$⊢{~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)$$
3		erdm	$$⊢{~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)\to \mathrm{dom}{~}_{𝑹}=𝑷\times 𝑷$$
4	2 3	ax-mp	$$⊢\mathrm{dom}{~}_{𝑹}=𝑷\times 𝑷$$
5		elqsn0	$$⊢\left(\mathrm{dom}{~}_{𝑹}=𝑷\times 𝑷\wedge \varnothing \in \left(\left(𝑷\times 𝑷\right)/{~}_{𝑹}\right)\right)\to \varnothing \ne \varnothing$$
6	4 5	mpan	$$⊢\varnothing \in \left(\left(𝑷\times 𝑷\right)/{~}_{𝑹}\right)\to \varnothing \ne \varnothing$$
7		df-nr	$$⊢𝑹=\left(𝑷\times 𝑷\right)/{~}_{𝑹}$$
8	6 7	eleq2s	$$⊢\varnothing \in 𝑹\to \varnothing \ne \varnothing$$
9	8	necon2bi	$$⊢\varnothing =\varnothing \to \neg \varnothing \in 𝑹$$
10	1 9	ax-mp	$$⊢\neg \varnothing \in 𝑹$$