Definition df-reap 8469

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 8476 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 8481). (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 8468	. 2 class #ℝ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1342	. . . . . 6 class 𝑥
4		cr 7748	. . . . . 6 class ℝ
5	3, 4	wcel 2136	. . . . 5 wff 𝑥 ∈ ℝ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1342	. . . . . 6 class 𝑦
8	7, 4	wcel 2136	. . . . 5 wff 𝑦 ∈ ℝ
9	5, 8	wa 103	. . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10		clt 7929	. . . . . 6 class <
11	3, 7, 10	wbr 3981	. . . . 5 wff 𝑥 < 𝑦
12	7, 3, 10	wbr 3981	. . . . 5 wff 𝑦 < 𝑥
13	11, 12	wo 698	. . . 4 wff (𝑥 < 𝑦 ∨ 𝑦 < 𝑥)
14	9, 13	wa 103	. . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))
15	14, 2, 6	copab 4041	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}
16	1, 15	wceq 1343	1 wff #ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦 ∨ 𝑦 < 𝑥))}

This definition is referenced by:  reapval  8470