Theorem elpqn 10838

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3044   class class class wbr 5095   × cxp 5621  ‘cfv 6486  2^nd c2nd 7930  Ncnpi 10757   <_N clti 10760   ~_Q ceq 10764  Qcnq 10765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-ss 3922  df-nq 10825

This theorem is referenced by:  nqereu  10842  nqerid  10846  enqeq  10847  addpqnq  10851  mulpqnq  10854  ordpinq  10856  addclnq  10858  mulclnq  10860  addnqf  10861  mulnqf  10862  adderpq  10869  mulerpq  10870  addassnq  10871  mulassnq  10872  distrnq  10874  mulidnq  10876  recmulnq  10877  ltsonq  10882  lterpq  10883  ltanq  10884  ltmnq  10885  ltexnq  10888  archnq  10893  wuncn  11083