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

Definition df-lt 10235
Description: Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 10366. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
Assertion
Ref Expression
df-lt < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-lt
StepHypRef Expression
1 cltrr 10226 . 2 class <
2 vx . . . . . . 7 setvar 𝑥
32cv 1652 . . . . . 6 class 𝑥
4 cr 10221 . . . . . 6 class
53, 4wcel 2157 . . . . 5 wff 𝑥 ∈ ℝ
6 vy . . . . . . 7 setvar 𝑦
76cv 1652 . . . . . 6 class 𝑦
87, 4wcel 2157 . . . . 5 wff 𝑦 ∈ ℝ
95, 8wa 385 . . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10 vz . . . . . . . . . . 11 setvar 𝑧
1110cv 1652 . . . . . . . . . 10 class 𝑧
12 c0r 9974 . . . . . . . . . 10 class 0R
1311, 12cop 4372 . . . . . . . . 9 class 𝑧, 0R
143, 13wceq 1653 . . . . . . . 8 wff 𝑥 = ⟨𝑧, 0R
15 vw . . . . . . . . . . 11 setvar 𝑤
1615cv 1652 . . . . . . . . . 10 class 𝑤
1716, 12cop 4372 . . . . . . . . 9 class 𝑤, 0R
187, 17wceq 1653 . . . . . . . 8 wff 𝑦 = ⟨𝑤, 0R
1914, 18wa 385 . . . . . . 7 wff (𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩)
20 cltr 9979 . . . . . . . 8 class <R
2111, 16, 20wbr 4841 . . . . . . 7 wff 𝑧 <R 𝑤
2219, 21wa 385 . . . . . 6 wff ((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)
2322, 15wex 1875 . . . . 5 wff 𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)
2423, 10wex 1875 . . . 4 wff 𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)
259, 24wa 385 . . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))
2625, 2, 6copab 4903 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
271, 26wceq 1653 1 wff < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Colors of variables: wff setvar class
This definition is referenced by:  ltrelre  10241  ltresr  10247
  Copyright terms: Public domain W3C validator