Theorem elpqn 10991

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145  ∀wral 3077   class class class wbr 5103   × cxp 5649  ‘cfv 6531  2^nd c2nd 7989  Ncnpi 10910   <_N clti 10913   ~_Q ceq 10917  Qcnq 10918

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-nq 10978

This theorem is used by:  nqereu  10995  nqerid  10999  enqeq  11000  addpqnq  11004  mulpqnq  11007  ordpinq  11009  addclnq  11011  mulclnq  11013  addnqf  11014  mulnqf  11015  adderpq  11022  mulerpq  11023  addassnq  11024  mulassnq  11025  distrnq  11027  mulidnq  11029  recmulnq  11030  ltsonq  11035  lterpq  11036  ltanq  11037  ltmnq  11038  ltexnq  11041  archnq  11046  wuncn  11236