Theorem elpqn 9333

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	|- ( A e. Q. -> A e. ( N. X. N. ) )

Proof of Theorem elpqn

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nq 9320	. . 3 |- Q. = { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) }
2		ssrab2 3524	. . 3 |- { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) } C_ ( N. X. N. )
3	1, 2	eqsstri 3472	. 2 |- Q. C_ ( N. X. N. )
4	3	sseli 3438	1 |- ( A e. Q. -> A e. ( N. X. N. ) )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1842   A.wral 2754   {crab 2758   class class class wbr 4395   X. cxp 4821   ` cfv 5569   2ndc2nd 6783   N.cnpi 9252   <N clti 9255   ~Q ceq 9259   Q.cnq 9260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-in 3421  df-ss 3428  df-nq 9320

This theorem is referenced by:  nqereu  9337  nqerid  9341  enqeq  9342  addpqnq  9346  mulpqnq  9349  ordpinq  9351  addclnq  9353  mulclnq  9355  addnqf  9356  mulnqf  9357  adderpq  9364  mulerpq  9365  addassnq  9366  mulassnq  9367  distrnq  9369  mulidnq  9371  recmulnq  9372  ltsonq  9377  lterpq  9378  ltanq  9379  ltmnq  9380  ltexnq  9383  archnq  9388  wuncn  9577