Theorem elpqn 9747

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 9734	. . 3 ⊢ Q = {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))}
2		ssrab2 3687	. . 3 ⊢ {𝑦 ∈ (N × N) ∣ ∀𝑥 ∈ (N × N)(𝑦 ~Q 𝑥 → ¬ (2nd ‘𝑥) <N (2nd ‘𝑦))} ⊆ (N × N)
3	1, 2	eqsstri 3635	. 2 ⊢ Q ⊆ (N × N)
4	3	sseli 3599	1 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1990  ∀wral 2912  {crab 2916   class class class wbr 4653   × cxp 5112  ‘cfv 5888  2^nd c2nd 7167  Ncnpi 9666   <_N clti 9669   ~_Q ceq 9673  Qcnq 9674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-nq 9734

This theorem is referenced by:  nqereu  9751  nqerid  9755  enqeq  9756  addpqnq  9760  mulpqnq  9763  ordpinq  9765  addclnq  9767  mulclnq  9769  addnqf  9770  mulnqf  9771  adderpq  9778  mulerpq  9779  addassnq  9780  mulassnq  9781  distrnq  9783  mulidnq  9785  recmulnq  9786  ltsonq  9791  lterpq  9792  ltanq  9793  ltmnq  9794  ltexnq  9797  archnq  9802  wuncn  9991