Definition df-lt 10884

Description: Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 11014. (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

Step	Hyp	Ref	Expression
1		cltrr 10875	. 2 class <ℝ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1538	. . . . . 6 class 𝑥
4		cr 10870	. . . . . 6 class ℝ
5	3, 4	wcel 2106	. . . . 5 wff 𝑥 ∈ ℝ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1538	. . . . . 6 class 𝑦
8	7, 4	wcel 2106	. . . . 5 wff 𝑦 ∈ ℝ
9	5, 8	wa 396	. . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10		vz	. . . . . . . . . . 11 setvar 𝑧
11	10	cv 1538	. . . . . . . . . 10 class 𝑧
12		c0r 10622	. . . . . . . . . 10 class 0R
13	11, 12	cop 4567	. . . . . . . . 9 class ⟨𝑧, 0R⟩
14	3, 13	wceq 1539	. . . . . . . 8 wff 𝑥 = ⟨𝑧, 0R⟩
15		vw	. . . . . . . . . . 11 setvar 𝑤
16	15	cv 1538	. . . . . . . . . 10 class 𝑤
17	16, 12	cop 4567	. . . . . . . . 9 class ⟨𝑤, 0R⟩
18	7, 17	wceq 1539	. . . . . . . 8 wff 𝑦 = ⟨𝑤, 0R⟩
19	14, 18	wa 396	. . . . . . 7 wff (𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩)
20		cltr 10627	. . . . . . . 8 class <R
21	11, 16, 20	wbr 5074	. . . . . . 7 wff 𝑧 <R 𝑤
22	19, 21	wa 396	. . . . . 6 wff ((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)
23	22, 15	wex 1782	. . . . 5 wff ∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)
24	23, 10	wex 1782	. . . 4 wff ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)
25	9, 24	wa 396	. . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))
26	25, 2, 6	copab 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
27	1, 26	wceq 1539	1 wff <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}

This definition is referenced by:  ltrelre  10890  ltresr  10896