Theorem ltrelnq 7173

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 7161	. 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 4613	. 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 3129	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 103   = wceq 1331   E.wex 1468   e. wcel 1480   C_ wss 3071   <.cop 3530   class class class wbr 3929   {copab 3988   X. cxp 4537  (class class class)co 5774   [cec 6427   .N cmi 7082   <N clti 7083   ~Q ceq 7087   Q.cnq 7088   <Q cltq 7093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-in 3077  df-ss 3084  df-opab 3990  df-xp 4545  df-ltnqqs 7161

This theorem is referenced by:  ltanqi  7210  ltmnqi  7211  lt2addnq  7212  lt2mulnq  7213  ltexnqi  7217  ltbtwnnqq  7223  ltbtwnnq  7224  prarloclemarch2  7227  ltrnqi  7229  prcdnql  7292  prcunqu  7293  prnmaxl  7296  prnminu  7297  prloc  7299  prarloclemcalc  7310  genplt2i  7318  genpcdl  7327  genpcuu  7328  genpdisj  7331  addnqprllem  7335  addnqprulem  7336  addlocprlemlt  7339  addlocprlemeq  7341  addlocprlemgt  7342  addlocprlem  7343  nqprdisj  7352  nqprloc  7353  nqprxx  7354  ltnqex  7357  gtnqex  7358  addnqprlemrl  7365  addnqprlemru  7366  addnqprlemfl  7367  addnqprlemfu  7368  appdivnq  7371  prmuloclemcalc  7373  prmuloc  7374  mulnqprlemrl  7381  mulnqprlemru  7382  mulnqprlemfl  7383  mulnqprlemfu  7384  1idprl  7398  1idpru  7399  ltnqpri  7402  ltsopr  7404  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemdisj  7414  ltexprlemloc  7415  ltexprlemfl  7417  ltexprlemru  7420  recexprlemell  7430  recexprlemelu  7431  recexprlemlol  7434  recexprlemupu  7436  recexprlemdisj  7438  recexprlemloc  7439  recexprlempr  7440  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemupu  7457  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  caucvgprlemk  7473  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemupu  7480  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprprlemloccalc  7492  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemupu  7508  caucvgprprlemloc  7511  suplocexprlemrl  7525  suplocexprlemru  7527