Theorem ltrelnq 7722

Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)

Assertion

Ref	Expression
ltrelnq	|- <Q C_ ( Q. X. Q. )

Proof of Theorem ltrelnq

Dummy variables x y z w u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ltnqqs 7710	. 2 |- <Q = { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) }
2		opabssxp 4844	. 2 |- { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) } C_ ( Q. X. Q. )
3	1, 2	eqsstri 3280	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1402   E.wex 1545   e. wcel 2209   C_ wss 3220   <.cop 3708   class class class wbr 4125   {copab 4186   X. cxp 4767  (class class class)co 6075   [cec 6795   .N cmi 7631   <N clti 7632   ~Q ceq 7636   Q.cnq 7637   <Q cltq 7642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-in 3226  df-ss 3233  df-opab 4188  df-xp 4775  df-ltnqqs 7710

This theorem is referenced by:  ltanqi  7759  ltmnqi  7760  lt2addnq  7761  lt2mulnq  7762  ltexnqi  7766  ltbtwnnqq  7772  ltbtwnnq  7773  prarloclemarch2  7776  ltrnqi  7778  prcdnql  7841  prcunqu  7842  prnmaxl  7845  prnminu  7846  prloc  7848  prarloclemcalc  7859  genplt2i  7867  genpcdl  7876  genpcuu  7877  genpdisj  7880  addnqprllem  7884  addnqprulem  7885  addlocprlemlt  7888  addlocprlemeq  7890  addlocprlemgt  7891  addlocprlem  7892  nqprdisj  7901  nqprloc  7902  nqprxx  7903  ltnqex  7906  gtnqex  7907  addnqprlemrl  7914  addnqprlemru  7915  addnqprlemfl  7916  addnqprlemfu  7917  appdivnq  7920  prmuloclemcalc  7922  prmuloc  7923  mulnqprlemrl  7930  mulnqprlemru  7931  mulnqprlemfl  7932  mulnqprlemfu  7933  1idprl  7947  1idpru  7948  ltnqpri  7951  ltsopr  7953  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemfl  7966  ltexprlemru  7969  recexprlemell  7979  recexprlemelu  7980  recexprlemlol  7983  recexprlemupu  7985  recexprlemdisj  7987  recexprlemloc  7988  recexprlempr  7989  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemupu  8006  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemk  8022  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemupu  8029  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprprlemloccalc  8041  caucvgprprlemml  8051  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemupu  8057  caucvgprprlemloc  8060  suplocexprlemrl  8074  suplocexprlemru  8076