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

Theorem ltrelsr 9768
 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 9760 . 2 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
2 opabssxp 5116 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))} ⊆ (R × R)
31, 2eqsstri 3598 1 <R ⊆ (R × R)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ⊆ wss 3540  ⟨cop 4131   class class class wbr 4583  {copab 4642   × cxp 5036  (class class class)co 6549  [cec 7627   +P cpp 9562
 Copyright terms: Public domain W3C validator