Theorem ltrelnq 6922

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 6910	. 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 4512	. 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 3056	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 102   = wceq 1289   E.wex 1426   e. wcel 1438   C_ wss 2999   <.cop 3449   class class class wbr 3845   {copab 3898   X. cxp 4436  (class class class)co 5652   [cec 6288   .N cmi 6831   <N clti 6832   ~Q ceq 6836   Q.cnq 6837   <Q cltq 6842

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-in 3005  df-ss 3012  df-opab 3900  df-xp 4444  df-ltnqqs 6910

This theorem is referenced by:  ltanqi  6959  ltmnqi  6960  lt2addnq  6961  lt2mulnq  6962  ltexnqi  6966  ltbtwnnqq  6972  ltbtwnnq  6973  prarloclemarch2  6976  ltrnqi  6978  prcdnql  7041  prcunqu  7042  prnmaxl  7045  prnminu  7046  prloc  7048  prarloclemcalc  7059  genplt2i  7067  genpcdl  7076  genpcuu  7077  genpdisj  7080  addnqprllem  7084  addnqprulem  7085  addlocprlemlt  7088  addlocprlemeq  7090  addlocprlemgt  7091  addlocprlem  7092  nqprdisj  7101  nqprloc  7102  nqprxx  7103  ltnqex  7106  gtnqex  7107  addnqprlemrl  7114  addnqprlemru  7115  addnqprlemfl  7116  addnqprlemfu  7117  appdivnq  7120  prmuloclemcalc  7122  prmuloc  7123  mulnqprlemrl  7130  mulnqprlemru  7131  mulnqprlemfl  7132  mulnqprlemfu  7133  1idprl  7147  1idpru  7148  ltnqpri  7151  ltsopr  7153  ltexprlemopl  7158  ltexprlemopu  7160  ltexprlemdisj  7163  ltexprlemloc  7164  ltexprlemfl  7166  ltexprlemru  7169  recexprlemell  7179  recexprlemelu  7180  recexprlemlol  7183  recexprlemupu  7185  recexprlemdisj  7187  recexprlemloc  7188  recexprlempr  7189  recexprlem1ssl  7190  recexprlem1ssu  7191  recexprlemss1l  7192  recexprlemss1u  7193  cauappcvgprlemm  7202  cauappcvgprlemopl  7203  cauappcvgprlemlol  7204  cauappcvgprlemupu  7206  cauappcvgprlemladdfu  7211  cauappcvgprlemladdfl  7212  caucvgprlemk  7222  caucvgprlemnkj  7223  caucvgprlemnbj  7224  caucvgprlemm  7225  caucvgprlemopl  7226  caucvgprlemlol  7227  caucvgprlemupu  7229  caucvgprlemloc  7232  caucvgprlemladdfu  7234  caucvgprprlemloccalc  7241  caucvgprprlemml  7251  caucvgprprlemopl  7254  caucvgprprlemlol  7255  caucvgprprlemupu  7257  caucvgprprlemloc  7260