Theorem elpqn 10612

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108  ∀wral 3063   class class class wbr 5070   × cxp 5578  ‘cfv 6418  2^nd c2nd 7803  Ncnpi 10531   <_N clti 10534   ~_Q ceq 10538  Qcnq 10539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-nq 10599

This theorem is referenced by:  nqereu  10616  nqerid  10620  enqeq  10621  addpqnq  10625  mulpqnq  10628  ordpinq  10630  addclnq  10632  mulclnq  10634  addnqf  10635  mulnqf  10636  adderpq  10643  mulerpq  10644  addassnq  10645  mulassnq  10646  distrnq  10648  mulidnq  10650  recmulnq  10651  ltsonq  10656  lterpq  10657  ltanq  10658  ltmnq  10659  ltexnq  10662  archnq  10667  wuncn  10857