Theorem elpqn

Description: Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	elpqn	$$⊢A\in 𝑸\to A\in \left(𝑵\times 𝑵\right)$$

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2	1	ssrab3	$$⊢𝑸\subseteq 𝑵\times 𝑵$$
3	2	sseli	$$⊢A\in 𝑸\to A\in \left(𝑵\times 𝑵\right)$$