Theorem elpqn 10994

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108  ∀wral 3067   class class class wbr 5166   × cxp 5698  ‘cfv 6573  2^nd c2nd 8029  Ncnpi 10913   <_N clti 10916   ~_Q ceq 10920  Qcnq 10921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-nq 10981

This theorem is referenced by:  nqereu  10998  nqerid  11002  enqeq  11003  addpqnq  11007  mulpqnq  11010  ordpinq  11012  addclnq  11014  mulclnq  11016  addnqf  11017  mulnqf  11018  adderpq  11025  mulerpq  11026  addassnq  11027  mulassnq  11028  distrnq  11030  mulidnq  11032  recmulnq  11033  ltsonq  11038  lterpq  11039  ltanq  11040  ltmnq  11041  ltexnq  11044  archnq  11049  wuncn  11239