Theorem elpqn 10813

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111  ∀wral 3047   class class class wbr 5091   × cxp 5614  ‘cfv 6481  2^nd c2nd 7920  Ncnpi 10732   <_N clti 10735   ~_Q ceq 10739  Qcnq 10740

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3919  df-nq 10800

This theorem is referenced by:  nqereu  10817  nqerid  10821  enqeq  10822  addpqnq  10826  mulpqnq  10829  ordpinq  10831  addclnq  10833  mulclnq  10835  addnqf  10836  mulnqf  10837  adderpq  10844  mulerpq  10845  addassnq  10846  mulassnq  10847  distrnq  10849  mulidnq  10851  recmulnq  10852  ltsonq  10857  lterpq  10858  ltanq  10859  ltmnq  10860  ltexnq  10863  archnq  10868  wuncn  11058