Theorem elpqn 9208

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 9195	. . 3 |- Q. = { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) <N ( 2nd ` y ) ) }
2		ssrab2 3548	. . 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 3497	. 2 |- Q. C_ ( N. X. N. )
4	3	sseli 3463	1 |- ( A e. Q. -> A e. ( N. X. N. ) )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1758   A.wral 2799   {crab 2803   class class class wbr 4403   X. cxp 4949   ` cfv 5529   2ndc2nd 6689   N.cnpi 9125   <N clti 9128   ~Q ceq 9132   Q.cnq 9133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-in 3446  df-ss 3453  df-nq 9195

This theorem is referenced by:  nqereu  9212  nqerid  9216  enqeq  9217  addpqnq  9221  mulpqnq  9224  ordpinq  9226  addclnq  9228  mulclnq  9230  addnqf  9231  mulnqf  9232  adderpq  9239  mulerpq  9240  addassnq  9241  mulassnq  9242  distrnq  9244  mulidnq  9246  recmulnq  9247  ltsonq  9252  lterpq  9253  ltanq  9254  ltmnq  9255  ltexnq  9258  archnq  9263  wuncn  9451