Theorem elpqn 10928

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146  ∀wral 3082   class class class wbr 5114   × cxp 5664  ‘cfv 6543  2^nd c2nd 7994  Ncnpi 10847   <_N clti 10850   ~_Q ceq 10854  Qcnq 10855

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-ss 3925  df-nq 10915

This theorem is used by:  nqereu  10932  nqerid  10936  enqeq  10937  addpqnq  10941  mulpqnq  10944  ordpinq  10946  addclnq  10948  mulclnq  10950  addnqf  10951  mulnqf  10952  adderpq  10959  mulerpq  10960  addassnq  10961  mulassnq  10962  distrnq  10964  mulidnq  10966  recmulnq  10967  ltsonq  10972  lterpq  10973  ltanq  10974  ltmnq  10975  ltexnq  10978  archnq  10983  wuncn  11173