Theorem elpqn 10938

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145  ∀wral 3078   class class class wbr 5107   × cxp 5657  ‘cfv 6537  2^nd c2nd 7989  Ncnpi 10857   <_N clti 10860   ~_Q ceq 10864  Qcnq 10865

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-nq 10925

This theorem is used by:  nqereu  10942  nqerid  10946  enqeq  10947  addpqnq  10951  mulpqnq  10954  ordpinq  10956  addclnq  10958  mulclnq  10960  addnqf  10961  mulnqf  10962  adderpq  10969  mulerpq  10970  addassnq  10971  mulassnq  10972  distrnq  10974  mulidnq  10976  recmulnq  10977  ltsonq  10982  lterpq  10983  ltanq  10984  ltmnq  10985  ltexnq  10988  archnq  10993  wuncn  11183