Theorem elpqn 10898

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2145  ∀wral 3079   class class class wbr 5105   × cxp 5650  ‘cfv 6525  2^nd c2nd 7973  Ncnpi 10817   <_N clti 10820   ~_Q ceq 10824  Qcnq 10825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-nq 10885

This theorem is referenced by:  nqereu  10902  nqerid  10906  enqeq  10907  addpqnq  10911  mulpqnq  10914  ordpinq  10916  addclnq  10918  mulclnq  10920  addnqf  10921  mulnqf  10922  adderpq  10929  mulerpq  10930  addassnq  10931  mulassnq  10932  distrnq  10934  mulidnq  10936  recmulnq  10937  ltsonq  10942  lterpq  10943  ltanq  10944  ltmnq  10945  ltexnq  10948  archnq  10953  wuncn  11143