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

Definition df-reap 7564
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 7571 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 7576). (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 7563 . 2 class #
2 vx . . . . . . 7 setvar 𝑥
32cv 1242 . . . . . 6 class 𝑥
4 cr 6886 . . . . . 6 class
53, 4wcel 1393 . . . . 5 wff 𝑥 ∈ ℝ
6 vy . . . . . . 7 setvar 𝑦
76cv 1242 . . . . . 6 class 𝑦
87, 4wcel 1393 . . . . 5 wff 𝑦 ∈ ℝ
95, 8wa 97 . . . 4 wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)
10 clt 7058 . . . . . 6 class <
113, 7, 10wbr 3764 . . . . 5 wff 𝑥 < 𝑦
127, 3, 10wbr 3764 . . . . 5 wff 𝑦 < 𝑥
1311, 12wo 629 . . . 4 wff (𝑥 < 𝑦𝑦 < 𝑥)
149, 13wa 97 . . 3 wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))
1514, 2, 6copab 3817 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
161, 15wceq 1243 1 wff # = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑥 < 𝑦𝑦 < 𝑥))}
Colors of variables: wff set class
This definition is referenced by:  reapval  7565
  Copyright terms: Public domain W3C validator