Theorem ltrelnq 7732

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 7720	. 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 4849	. 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. )

This proof depends on syntax axioms:   /\ wa 104   = wceq 1402   E.wex 1545   e. wcel 2209   C_ wss 3220   <.cop 3712   class class class wbr 4130   {copab 4191   X. cxp 4772  (class class class)co 6085   [cec 6805   .N cmi 7641   <N clti 7642   ~Q ceq 7646   Q.cnq 7647   <Q cltq 7652

This proof depends on 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 proof 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 4193  df-xp 4780  df-ltnqqs 7720

This theorem is used by:  ltanqi  7769  ltmnqi  7770  lt2addnq  7771  lt2mulnq  7772  ltexnqi  7776  ltbtwnnqq  7782  ltbtwnnq  7783  prarloclemarch2  7786  ltrnqi  7788  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  prloc  7858  prarloclemcalc  7869  genplt2i  7877  genpcdl  7886  genpcuu  7887  genpdisj  7890  addnqprllem  7894  addnqprulem  7895  addlocprlemlt  7898  addlocprlemeq  7900  addlocprlemgt  7901  addlocprlem  7902  nqprdisj  7911  nqprloc  7912  nqprxx  7913  ltnqex  7916  gtnqex  7917  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  1idprl  7957  1idpru  7958  ltnqpri  7961  ltsopr  7963  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemru  7979  recexprlemell  7989  recexprlemelu  7990  recexprlemlol  7993  recexprlemupu  7995  recexprlemdisj  7997  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemk  8032  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprprlemloccalc  8051  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemupu  8067  caucvgprprlemloc  8070  suplocexprlemrl  8084  suplocexprlemru  8086