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

Definition df-reap 8481
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 8488 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 8493). (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 8480 . 2 class #
2 vx . . . . . . 7 setvar 𝑥
32cv 1347 . . . . . 6 class 𝑥
4 cr 7760 . . . . . 6 class
53, 4wcel 2141 . . . . 5 wff 𝑥 ∈ ℝ
6 vy . . . . . . 7 setvar 𝑦
76cv 1347 . . . . . 6 class 𝑦
87, 4wcel 2141 . . . . 5 wff 𝑦 ∈ ℝ
95, 8wa 103 . . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10 clt 7941 . . . . . 6 class <
113, 7, 10wbr 3987 . . . . 5 wff 𝑥 < 𝑦
127, 3, 10wbr 3987 . . . . 5 wff 𝑦 < 𝑥
1311, 12wo 703 . . . 4 wff (𝑥 < 𝑦𝑦 < 𝑥)
149, 13wa 103 . . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))
1514, 2, 6copab 4047 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
161, 15wceq 1348 1 wff # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
Colors of variables: wff set class
This definition is referenced by:  reapval  8482
  Copyright terms: Public domain W3C validator