Theorem elpqn 11013

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144  ∀wral 3076   class class class wbr 5102   × cxp 5648  ‘cfv 6538  2^nd c2nd 8000  Ncnpi 10932   <_N clti 10935   ~_Q ceq 10939  Qcnq 10940

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-nq 11000

This theorem is used by:  nqereu  11017  nqerid  11021  enqeq  11022  addpqnq  11026  mulpqnq  11029  ordpinq  11031  addclnq  11033  mulclnq  11035  addnqf  11036  mulnqf  11037  adderpq  11044  mulerpq  11045  addassnq  11046  mulassnq  11047  distrnq  11049  mulidnq  11051  recmulnq  11052  ltsonq  11057  lterpq  11058  ltanq  11059  ltmnq  11060  ltexnq  11063  archnq  11068  wuncn  11258