Theorem elpqn 10954

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 10941	. . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
2	1	ssrab3 4078	. 2 ⊢ Q ⊆ (N × N)
3	2	sseli 3976	1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2098  ∀wral 3057   class class class wbr 5150   × cxp 5678  ‘cfv 6551  2^nd c2nd 7996  Ncnpi 10873   <_N clti 10876   ~_Q ceq 10880  Qcnq 10881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-in 3954  df-ss 3964  df-nq 10941

This theorem is referenced by:  nqereu  10958  nqerid  10962  enqeq  10963  addpqnq  10967  mulpqnq  10970  ordpinq  10972  addclnq  10974  mulclnq  10976  addnqf  10977  mulnqf  10978  adderpq  10985  mulerpq  10986  addassnq  10987  mulassnq  10988  distrnq  10990  mulidnq  10992  recmulnq  10993  ltsonq  10998  lterpq  10999  ltanq  11000  ltmnq  11001  ltexnq  11004  archnq  11009  wuncn  11199