Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-reap GIF version

Definition df-reap 7640
 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 7647 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 7652). (Contributed by Jim Kingdon, 26-Jan-2020.)
Assertion
Ref Expression
df-reap # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-reap
StepHypRef Expression
1 creap 7639 . 2 class #
2 vx . . . . . . 7 setvar 𝑥
32cv 1258 . . . . . 6 class 𝑥
4 cr 6946 . . . . . 6 class
53, 4wcel 1409 . . . . 5 wff 𝑥 ∈ ℝ
6 vy . . . . . . 7 setvar 𝑦
76cv 1258 . . . . . 6 class 𝑦
87, 4wcel 1409 . . . . 5 wff 𝑦 ∈ ℝ
95, 8wa 101 . . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10 clt 7119 . . . . . 6 class <
113, 7, 10wbr 3792 . . . . 5 wff 𝑥 < 𝑦
127, 3, 10wbr 3792 . . . . 5 wff 𝑦 < 𝑥
1311, 12wo 639 . . . 4 wff (𝑥 < 𝑦𝑦 < 𝑥)
149, 13wa 101 . . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))
1514, 2, 6copab 3845 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
161, 15wceq 1259 1 wff # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
 Colors of variables: wff set class This definition is referenced by:  reapval  7641
 Copyright terms: Public domain W3C validator