Theorem ltrelnq 7584

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 7572	. 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 4800	. 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 3259	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1397   E.wex 1540   e. wcel 2202   C_ wss 3200   <.cop 3672   class class class wbr 4088   {copab 4149   X. cxp 4723  (class class class)co 6017   [cec 6699   .N cmi 7493   <N clti 7494   ~Q ceq 7498   Q.cnq 7499   <Q cltq 7504

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-in 3206  df-ss 3213  df-opab 4151  df-xp 4731  df-ltnqqs 7572

This theorem is referenced by:  ltanqi  7621  ltmnqi  7622  lt2addnq  7623  lt2mulnq  7624  ltexnqi  7628  ltbtwnnqq  7634  ltbtwnnq  7635  prarloclemarch2  7638  ltrnqi  7640  prcdnql  7703  prcunqu  7704  prnmaxl  7707  prnminu  7708  prloc  7710  prarloclemcalc  7721  genplt2i  7729  genpcdl  7738  genpcuu  7739  genpdisj  7742  addnqprllem  7746  addnqprulem  7747  addlocprlemlt  7750  addlocprlemeq  7752  addlocprlemgt  7753  addlocprlem  7754  nqprdisj  7763  nqprloc  7764  nqprxx  7765  ltnqex  7768  gtnqex  7769  addnqprlemrl  7776  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  appdivnq  7782  prmuloclemcalc  7784  prmuloc  7785  mulnqprlemrl  7792  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  1idprl  7809  1idpru  7810  ltnqpri  7813  ltsopr  7815  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemru  7831  recexprlemell  7841  recexprlemelu  7842  recexprlemlol  7845  recexprlemupu  7847  recexprlemdisj  7849  recexprlemloc  7850  recexprlempr  7851  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemupu  7868  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemk  7884  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemupu  7891  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprprlemloccalc  7903  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemupu  7919  caucvgprprlemloc  7922  suplocexprlemrl  7936  suplocexprlemru  7938