Theorem ltrelnq 7575

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 7563	. 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 4798	. 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 3257	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1395   E.wex 1538   e. wcel 2200   C_ wss 3198   <.cop 3670   class class class wbr 4086   {copab 4147   X. cxp 4721  (class class class)co 6013   [cec 6695   .N cmi 7484   <N clti 7485   ~Q ceq 7489   Q.cnq 7490   <Q cltq 7495

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3204  df-ss 3211  df-opab 4149  df-xp 4729  df-ltnqqs 7563

This theorem is referenced by:  ltanqi  7612  ltmnqi  7613  lt2addnq  7614  lt2mulnq  7615  ltexnqi  7619  ltbtwnnqq  7625  ltbtwnnq  7626  prarloclemarch2  7629  ltrnqi  7631  prcdnql  7694  prcunqu  7695  prnmaxl  7698  prnminu  7699  prloc  7701  prarloclemcalc  7712  genplt2i  7720  genpcdl  7729  genpcuu  7730  genpdisj  7733  addnqprllem  7737  addnqprulem  7738  addlocprlemlt  7741  addlocprlemeq  7743  addlocprlemgt  7744  addlocprlem  7745  nqprdisj  7754  nqprloc  7755  nqprxx  7756  ltnqex  7759  gtnqex  7760  addnqprlemrl  7767  addnqprlemru  7768  addnqprlemfl  7769  addnqprlemfu  7770  appdivnq  7773  prmuloclemcalc  7775  prmuloc  7776  mulnqprlemrl  7783  mulnqprlemru  7784  mulnqprlemfl  7785  mulnqprlemfu  7786  1idprl  7800  1idpru  7801  ltnqpri  7804  ltsopr  7806  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemfl  7819  ltexprlemru  7822  recexprlemell  7832  recexprlemelu  7833  recexprlemlol  7836  recexprlemupu  7838  recexprlemdisj  7840  recexprlemloc  7841  recexprlempr  7842  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemupu  7859  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemk  7875  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemupu  7882  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprprlemloccalc  7894  caucvgprprlemml  7904  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemupu  7910  caucvgprprlemloc  7913  suplocexprlemrl  7927  suplocexprlemru  7929