Theorem elpqn 10944

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3052   class class class wbr 5124   × cxp 5657  ‘cfv 6536  2^nd c2nd 7992  Ncnpi 10863   <_N clti 10866   ~_Q ceq 10870  Qcnq 10871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-ss 3948  df-nq 10931

This theorem is referenced by:  nqereu  10948  nqerid  10952  enqeq  10953  addpqnq  10957  mulpqnq  10960  ordpinq  10962  addclnq  10964  mulclnq  10966  addnqf  10967  mulnqf  10968  adderpq  10975  mulerpq  10976  addassnq  10977  mulassnq  10978  distrnq  10980  mulidnq  10982  recmulnq  10983  ltsonq  10988  lterpq  10989  ltanq  10990  ltmnq  10991  ltexnq  10994  archnq  10999  wuncn  11189