Theorem elpqn 10082

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.)

Assertion

Ref	Expression
elpqn	⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Proof of Theorem elpqn

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nq 10069	. . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
2	1	ssrab3 3909	. 2 ⊢ Q ⊆ (N × N)
3	2	sseli 3817	1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107  ∀wral 3090   class class class wbr 4886   × cxp 5353  ‘cfv 6135  2^nd c2nd 7444  Ncnpi 10001   <_N clti 10004   ~_Q ceq 10008  Qcnq 10009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-in 3799  df-ss 3806  df-nq 10069

This theorem is referenced by:  nqereu  10086  nqerid  10090  enqeq  10091  addpqnq  10095  mulpqnq  10098  ordpinq  10100  addclnq  10102  mulclnq  10104  addnqf  10105  mulnqf  10106  adderpq  10113  mulerpq  10114  addassnq  10115  mulassnq  10116  distrnq  10118  mulidnq  10120  recmulnq  10121  ltsonq  10126  lterpq  10127  ltanq  10128  ltmnq  10129  ltexnq  10132  archnq  10137  wuncn  10327