Theorem elpqn 10911

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143  ∀wral 3079   class class class wbr 5110   × cxp 5661  ‘cfv 6538  2^nd c2nd 7986  Ncnpi 10830   <_N clti 10833   ~_Q ceq 10837  Qcnq 10838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923  df-nq 10898

This theorem is referenced by:  nqereu  10915  nqerid  10919  enqeq  10920  addpqnq  10924  mulpqnq  10927  ordpinq  10929  addclnq  10931  mulclnq  10933  addnqf  10934  mulnqf  10935  adderpq  10942  mulerpq  10943  addassnq  10944  mulassnq  10945  distrnq  10947  mulidnq  10949  recmulnq  10950  ltsonq  10955  lterpq  10956  ltanq  10957  ltmnq  10958  ltexnq  10961  archnq  10966  wuncn  11156