Theorem elpqn 10846

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119  ∀wral 3054   class class class wbr 5079   × cxp 5623  ‘cfv 6492  2^nd c2nd 7937  Ncnpi 10765   <_N clti 10768   ~_Q ceq 10772  Qcnq 10773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-ss 3907  df-nq 10833

This theorem is referenced by:  nqereu  10850  nqerid  10854  enqeq  10855  addpqnq  10859  mulpqnq  10862  ordpinq  10864  addclnq  10866  mulclnq  10868  addnqf  10869  mulnqf  10870  adderpq  10877  mulerpq  10878  addassnq  10879  mulassnq  10880  distrnq  10882  mulidnq  10884  recmulnq  10885  ltsonq  10890  lterpq  10891  ltanq  10892  ltmnq  10893  ltexnq  10896  archnq  10901  wuncn  11091