Theorem 0nnq

Description: The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995) (Revised by Mario Carneiro, 27-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	0nnq	$$⊢\neg \varnothing \in 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		0nelxp	$$⊢\neg \varnothing \in \left(𝑵\times 𝑵\right)$$
2		df-nq	$$⊢𝑸=\left\{y\in \left(𝑵\times 𝑵\right)|\forall x\in \left(𝑵\times 𝑵\right)\left(y{~}_{𝑸}x\to \neg 2^{nd}\left(x\right){<}_{𝑵}{2}^{nd}\left(y\right)\right)\right\}$$
3	2	ssrab3	$$⊢𝑸\subseteq 𝑵\times 𝑵$$
4	3	sseli	$$⊢\varnothing \in 𝑸\to \varnothing \in \left(𝑵\times 𝑵\right)$$
5	1 4	mto	$$⊢\neg \varnothing \in 𝑸$$