Definition df-lt 4041

Description: Define 'less than' on the real subset of complex numbers.

Assertion

Ref	Expression
df-lt	⊢ < = {⟨x, y⟩∣((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w))}

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Definition df-lt

Step	Hyp	Ref	Expression
1		clt 4033	. 2 class <
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cr 4027	. . . . . 6 class ℝ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ ℝ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ ℝ
9	5, 8	wa 196	. . . 4 wff (x ∈ ℝ ∧ y ∈ ℝ)
10		vz	. . . . . . . . . . 11 set z
11	10	cv 1089	. . . . . . . . . 10 class z
12		c0r 3788	. . . . . . . . . 10 class 0R
13	11, 12	cop 1810	. . . . . . . . 9 class ⟨z, 0R⟩
14	3, 13	wceq 1091	. . . . . . . 8 wff x = ⟨z, 0R⟩
15		vw	. . . . . . . . . . 11 set w
16	15	cv 1089	. . . . . . . . . 10 class w
17	16, 12	cop 1810	. . . . . . . . 9 class ⟨w, 0R⟩
18	7, 17	wceq 1091	. . . . . . . 8 wff y = ⟨w, 0R⟩
19	14, 18	wa 196	. . . . . . 7 wff (x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩)
20		cltr 3793	. . . . . . . 8 class <R
21	11, 16, 20	wbr 2054	. . . . . . 7 wff z <R w
22	19, 21	wa 196	. . . . . 6 wff ((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w)
23	22, 15	wex 678	. . . . 5 wff ∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w)
24	23, 10	wex 678	. . . 4 wff ∃z∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w)
25	9, 24	wa 196	. . 3 wff ((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w))
26	25, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w))}
27	1, 26	wceq 1091	1 wff < = {⟨x, y⟩∣((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = ⟨z, 0R⟩ ∧ y = ⟨w, 0R⟩) ∧ z <R w))}

This definition is referenced by:  ltrelre 4046  ltresr 4052

metamath.org