Definition df-reap 8494

Description: Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although #_ℝ is an apartness relation on the reals (see df-ap 8501 for more discussion of apartness relations), for our purposes it is just a stepping stone to defining # which is an apartness relation on complex numbers. On the reals, #_ℝ and # agree (apreap 8506). (Contributed by Jim Kingdon, 26-Jan-2020.)

Assertion

Ref	Expression
df-reap	⊢ #ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-reap

Step	Hyp	Ref	Expression
1		creap 8493	. 2 class #ℝ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1347	. . . . . 6 class 𝑥
4		cr 7773	. . . . . 6 class ℝ
5	3, 4	wcel 2141	. . . . 5 wff 𝑥 ∈ ℝ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1347	. . . . . 6 class 𝑦
8	7, 4	wcel 2141	. . . . 5 wff 𝑦 ∈ ℝ
9	5, 8	wa 103	. . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10		clt 7954	. . . . . 6 class <
11	3, 7, 10	wbr 3989	. . . . 5 wff 𝑥 < 𝑦
12	7, 3, 10	wbr 3989	. . . . 5 wff 𝑦 < 𝑥
13	11, 12	wo 703	. . . 4 wff (𝑥 < 𝑦 ∨ 𝑦 < 𝑥)
14	9, 13	wa 103	. . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))
15	14, 2, 6	copab 4049	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}
16	1, 15	wceq 1348	1 wff #ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}

This definition is referenced by:  reapval  8495