Theorem elpqn 10848

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114  ∀wral 3051   class class class wbr 5085   × cxp 5629  ‘cfv 6498  2^nd c2nd 7941  Ncnpi 10767   <_N clti 10770   ~_Q ceq 10774  Qcnq 10775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-nq 10835

This theorem is referenced by:  nqereu  10852  nqerid  10856  enqeq  10857  addpqnq  10861  mulpqnq  10864  ordpinq  10866  addclnq  10868  mulclnq  10870  addnqf  10871  mulnqf  10872  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltsonq  10892  lterpq  10893  ltanq  10894  ltmnq  10895  ltexnq  10898  archnq  10903  wuncn  11093