Theorem ltrelnq 7395

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 7383	. 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 4718	. 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 3202	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1364   E.wex 1503   e. wcel 2160   C_ wss 3144   <.cop 3610   class class class wbr 4018   {copab 4078   X. cxp 4642  (class class class)co 5897   [cec 6558   .N cmi 7304   <N clti 7305   ~Q ceq 7309   Q.cnq 7310   <Q cltq 7315

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-in 3150  df-ss 3157  df-opab 4080  df-xp 4650  df-ltnqqs 7383

This theorem is referenced by:  ltanqi  7432  ltmnqi  7433  lt2addnq  7434  lt2mulnq  7435  ltexnqi  7439  ltbtwnnqq  7445  ltbtwnnq  7446  prarloclemarch2  7449  ltrnqi  7451  prcdnql  7514  prcunqu  7515  prnmaxl  7518  prnminu  7519  prloc  7521  prarloclemcalc  7532  genplt2i  7540  genpcdl  7549  genpcuu  7550  genpdisj  7553  addnqprllem  7557  addnqprulem  7558  addlocprlemlt  7561  addlocprlemeq  7563  addlocprlemgt  7564  addlocprlem  7565  nqprdisj  7574  nqprloc  7575  nqprxx  7576  ltnqex  7579  gtnqex  7580  addnqprlemrl  7587  addnqprlemru  7588  addnqprlemfl  7589  addnqprlemfu  7590  appdivnq  7593  prmuloclemcalc  7595  prmuloc  7596  mulnqprlemrl  7603  mulnqprlemru  7604  mulnqprlemfl  7605  mulnqprlemfu  7606  1idprl  7620  1idpru  7621  ltnqpri  7624  ltsopr  7626  ltexprlemopl  7631  ltexprlemopu  7633  ltexprlemdisj  7636  ltexprlemloc  7637  ltexprlemfl  7639  ltexprlemru  7642  recexprlemell  7652  recexprlemelu  7653  recexprlemlol  7656  recexprlemupu  7658  recexprlemdisj  7660  recexprlemloc  7661  recexprlempr  7662  recexprlem1ssl  7663  recexprlem1ssu  7664  recexprlemss1l  7665  recexprlemss1u  7666  cauappcvgprlemm  7675  cauappcvgprlemopl  7676  cauappcvgprlemlol  7677  cauappcvgprlemupu  7679  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  caucvgprlemk  7695  caucvgprlemnkj  7696  caucvgprlemnbj  7697  caucvgprlemm  7698  caucvgprlemopl  7699  caucvgprlemlol  7700  caucvgprlemupu  7702  caucvgprlemloc  7705  caucvgprlemladdfu  7707  caucvgprprlemloccalc  7714  caucvgprprlemml  7724  caucvgprprlemopl  7727  caucvgprprlemlol  7728  caucvgprprlemupu  7730  caucvgprprlemloc  7733  suplocexprlemrl  7747  suplocexprlemru  7749