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

Theorem ltrelsr 11106
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 11097 . 2 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
2 opabssxp 5781 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))} ⊆ (R × R)
31, 2eqsstri 4030 1 <R ⊆ (R × R)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1537  wex 1776  wcel 2106  wss 3963  cop 4637   class class class wbr 5148  {copab 5210   × cxp 5687  (class class class)co 7431  [cec 8742   +P cpp 10899  <P cltp 10901   ~R cer 10902  Rcnr 10903   <R cltr 10909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-ss 3980  df-opab 5211  df-xp 5695  df-ltr 11097
This theorem is referenced by:  ltsrpr  11115  ltasr  11138  recexsrlem  11141  addgt0sr  11142  mulgt0sr  11143  map2psrpr  11148  supsrlem  11149  supsr  11150  ltresr  11178  axpre-lttrn  11204
  Copyright terms: Public domain W3C validator