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

Theorem ltrelnq 10346
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 10338 . 2 <Q = ( <pQ ∩ (Q × Q))
2 inss2 4191 . 2 ( <pQ ∩ (Q × Q)) ⊆ (Q × Q)
31, 2eqsstri 3987 1 <Q ⊆ (Q × Q)
Colors of variables: wff setvar class
Syntax hints:  cin 3918  wss 3919   × cxp 5540   <pQ cltpq 10270  Qcnq 10272   <Q cltq 10278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-in 3926  df-ss 3936  df-ltnq 10338
This theorem is referenced by:  lterpq  10390  ltanq  10391  ltmnq  10392  ltexnq  10395  ltbtwnnq  10398  ltrnq  10399  prcdnq  10413  prnmadd  10417  genpcd  10426  nqpr  10434  1idpr  10449  prlem934  10453  ltexprlem4  10459  prlem936  10467  reclem2pr  10468  reclem3pr  10469  reclem4pr  10470
  Copyright terms: Public domain W3C validator