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

Theorem ltrelsr 9745
Description: Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ltrelsr <R ⊆ (R × R)

Proof of Theorem ltrelsr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ltr 9737 . 2 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
2 opabssxp 5106 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))} ⊆ (R × R)
31, 2eqsstri 3597 1 <R ⊆ (R × R)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wex 1694  wcel 1976  wss 3539  cop 4130   class class class wbr 4577  {copab 4636   × cxp 5026  (class class class)co 6527  [cec 7604   +P cpp 9539  <P cltp 9541   ~R cer 9542  Rcnr 9543   <R cltr 9549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553  df-opab 4638  df-xp 5034  df-ltr 9737
This theorem is referenced by:  ltsrpr  9754  ltasr  9777  recexsrlem  9780  addgt0sr  9781  mulgt0sr  9782  map2psrpr  9787  supsrlem  9788  supsr  9789  ltresr  9817  axpre-lttrn  9843
  Copyright terms: Public domain W3C validator