Theorem elpqn 10836

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113  ∀wral 3051   class class class wbr 5098   × cxp 5622  ‘cfv 6492  2^nd c2nd 7932  Ncnpi 10755   <_N clti 10758   ~_Q ceq 10762  Qcnq 10763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918  df-nq 10823

This theorem is referenced by:  nqereu  10840  nqerid  10844  enqeq  10845  addpqnq  10849  mulpqnq  10852  ordpinq  10854  addclnq  10856  mulclnq  10858  addnqf  10859  mulnqf  10860  adderpq  10867  mulerpq  10868  addassnq  10869  mulassnq  10870  distrnq  10872  mulidnq  10874  recmulnq  10875  ltsonq  10880  lterpq  10881  ltanq  10882  ltmnq  10883  ltexnq  10886  archnq  10891  wuncn  11081