Metamath Proof Explorer

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 \emptyset \in 𝑹$

Proof

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