MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltrelnq Structured version   Visualization version   GIF version

Theorem ltrelnq 10083
Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ltrelnq <Q ⊆ (Q × Q)

Proof of Theorem ltrelnq
StepHypRef Expression
1 df-ltnq 10075 . 2 <Q = ( <pQ ∩ (Q × Q))
2 inss2 4054 . 2 ( <pQ ∩ (Q × Q)) ⊆ (Q × Q)
31, 2eqsstri 3854 1 <Q ⊆ (Q × Q)
Colors of variables: wff setvar class
Syntax hints:  cin 3791  wss 3792   × cxp 5353   <pQ cltpq 10007  Qcnq 10009   <Q cltq 10015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ss 3806  df-ltnq 10075
This theorem is referenced by:  lterpq  10127  ltanq  10128  ltmnq  10129  ltexnq  10132  ltbtwnnq  10135  ltrnq  10136  prcdnq  10150  prnmadd  10154  genpcd  10163  nqpr  10171  1idpr  10186  prlem934  10190  ltexprlem4  10196  prlem936  10204  reclem2pr  10205  reclem3pr  10206  reclem4pr  10207
  Copyright terms: Public domain W3C validator