Theorem elpqn 10878

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3044   class class class wbr 5107   × cxp 5636  ‘cfv 6511  2^nd c2nd 7967  Ncnpi 10797   <_N clti 10800   ~_Q ceq 10804  Qcnq 10805

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 3406  df-ss 3931  df-nq 10865

This theorem is referenced by:  nqereu  10882  nqerid  10886  enqeq  10887  addpqnq  10891  mulpqnq  10894  ordpinq  10896  addclnq  10898  mulclnq  10900  addnqf  10901  mulnqf  10902  adderpq  10909  mulerpq  10910  addassnq  10911  mulassnq  10912  distrnq  10914  mulidnq  10916  recmulnq  10917  ltsonq  10922  lterpq  10923  ltanq  10924  ltmnq  10925  ltexnq  10928  archnq  10933  wuncn  11123