Theorem elpqn 9368

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 9355	. . 3 |- Q. = { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) }
2		ssrab2 3500	. . 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 3448	. 2 |- Q. C_ ( N. X. N. )
4	3	sseli 3414	1 |- ( A e. Q. -> A e. ( N. X. N. ) )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1904   A.wral 2756   {crab 2760   class class class wbr 4395   X. cxp 4837   ` cfv 5589   2ndc2nd 6811   N.cnpi 9287   <N clti 9290   ~Q ceq 9294   Q.cnq 9295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-in 3397  df-ss 3404  df-nq 9355

This theorem is referenced by:  nqereu  9372  nqerid  9376  enqeq  9377  addpqnq  9381  mulpqnq  9384  ordpinq  9386  addclnq  9388  mulclnq  9390  addnqf  9391  mulnqf  9392  adderpq  9399  mulerpq  9400  addassnq  9401  mulassnq  9402  distrnq  9404  mulidnq  9406  recmulnq  9407  ltsonq  9412  lterpq  9413  ltanq  9414  ltmnq  9415  ltexnq  9418  archnq  9423  wuncn  9612