ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltrelnq Unicode version

Theorem ltrelnq 7166
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.
StepHypRef Expression
1 df-ltnqqs 7154 . 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 4608 . 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. )
31, 2eqsstri 3124 1  |-  <Q  C_  ( Q.  X.  Q. )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    = wceq 1331   E.wex 1468    e. wcel 1480    C_ wss 3066   <.cop 3525   class class class wbr 3924   {copab 3983    X. cxp 4532  (class class class)co 5767   [cec 6420    .N cmi 7075    <N clti 7076    ~Q ceq 7080   Q.cnq 7081    <Q cltq 7086
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 2119
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-in 3072  df-ss 3079  df-opab 3985  df-xp 4540  df-ltnqqs 7154
This theorem is referenced by:  ltanqi  7203  ltmnqi  7204  lt2addnq  7205  lt2mulnq  7206  ltexnqi  7210  ltbtwnnqq  7216  ltbtwnnq  7217  prarloclemarch2  7220  ltrnqi  7222  prcdnql  7285  prcunqu  7286  prnmaxl  7289  prnminu  7290  prloc  7292  prarloclemcalc  7303  genplt2i  7311  genpcdl  7320  genpcuu  7321  genpdisj  7324  addnqprllem  7328  addnqprulem  7329  addlocprlemlt  7332  addlocprlemeq  7334  addlocprlemgt  7335  addlocprlem  7336  nqprdisj  7345  nqprloc  7346  nqprxx  7347  ltnqex  7350  gtnqex  7351  addnqprlemrl  7358  addnqprlemru  7359  addnqprlemfl  7360  addnqprlemfu  7361  appdivnq  7364  prmuloclemcalc  7366  prmuloc  7367  mulnqprlemrl  7374  mulnqprlemru  7375  mulnqprlemfl  7376  mulnqprlemfu  7377  1idprl  7391  1idpru  7392  ltnqpri  7395  ltsopr  7397  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemfl  7410  ltexprlemru  7413  recexprlemell  7423  recexprlemelu  7424  recexprlemlol  7427  recexprlemupu  7429  recexprlemdisj  7431  recexprlemloc  7432  recexprlempr  7433  recexprlem1ssl  7434  recexprlem1ssu  7435  recexprlemss1l  7436  recexprlemss1u  7437  cauappcvgprlemm  7446  cauappcvgprlemopl  7447  cauappcvgprlemlol  7448  cauappcvgprlemupu  7450  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  caucvgprlemk  7466  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemm  7469  caucvgprlemopl  7470  caucvgprlemlol  7471  caucvgprlemupu  7473  caucvgprlemloc  7476  caucvgprlemladdfu  7478  caucvgprprlemloccalc  7485  caucvgprprlemml  7495  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemupu  7501  caucvgprprlemloc  7504  suplocexprlemrl  7518  suplocexprlemru  7520
  Copyright terms: Public domain W3C validator