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

Theorem ltrelnq 10967
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 10959 . 2 <Q = ( <pQ ∩ (Q × Q))
2 inss2 4237 . 2 ( <pQ ∩ (Q × Q)) ⊆ (Q × Q)
31, 2eqsstri 4029 1 <Q ⊆ (Q × Q)
Colors of variables: wff setvar class
Syntax hints:  cin 3949  wss 3950   × cxp 5682   <pQ cltpq 10891  Qcnq 10893   <Q cltq 10899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-in 3957  df-ss 3967  df-ltnq 10959
This theorem is referenced by:  lterpq  11011  ltanq  11012  ltmnq  11013  ltexnq  11016  ltbtwnnq  11019  ltrnq  11020  prcdnq  11034  prnmadd  11038  genpcd  11047  nqpr  11055  1idpr  11070  prlem934  11074  ltexprlem4  11080  prlem936  11088  reclem2pr  11089  reclem3pr  11090  reclem4pr  11091
  Copyright terms: Public domain W3C validator