Theorem elpqn 11040

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147  ∀wral 3080   class class class wbr 5106   × cxp 5654  ‘cfv 6561  2^nd c2nd 8027  Ncnpi 10959   <_N clti 10962   ~_Q ceq 10966  Qcnq 10967

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-nq 11027

This theorem is used by:  nqereu  11044  nqerid  11048  enqeq  11049  addpqnq  11053  mulpqnq  11056  ordpinq  11058  addclnq  11060  mulclnq  11062  addnqf  11063  mulnqf  11064  adderpq  11071  mulerpq  11072  addassnq  11073  mulassnq  11074  distrnq  11076  mulidnq  11078  recmulnq  11079  ltsonq  11084  lterpq  11085  ltanq  11086  ltmnq  11087  ltexnq  11090  archnq  11095  wuncn  11285