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

Definition df-reap 7339
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 7346 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 7351). (Contributed by Jim Kingdon, 26-Jan-2020.)
Assertion
Ref Expression
df-reap # = {⟨x, y⟩ ∣ ((x y ℝ) (x < y y < x))}
Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-reap
StepHypRef Expression
1 creap 7338 . 2 class #
2 vx . . . . . . 7 setvar x
32cv 1241 . . . . . 6 class x
4 cr 6690 . . . . . 6 class
53, 4wcel 1390 . . . . 5 wff x
6 vy . . . . . . 7 setvar y
76cv 1241 . . . . . 6 class y
87, 4wcel 1390 . . . . 5 wff y
95, 8wa 97 . . . 4 wff (x y ℝ)
10 clt 6837 . . . . . 6 class <
113, 7, 10wbr 3755 . . . . 5 wff x < y
127, 3, 10wbr 3755 . . . . 5 wff y < x
1311, 12wo 628 . . . 4 wff (x < y y < x)
149, 13wa 97 . . 3 wff ((x y ℝ) (x < y y < x))
1514, 2, 6copab 3808 . 2 class {⟨x, y⟩ ∣ ((x y ℝ) (x < y y < x))}
161, 15wceq 1242 1 wff # = {⟨x, y⟩ ∣ ((x y ℝ) (x < y y < x))}
Colors of variables: wff set class
This definition is referenced by:  reapval  7340
  Copyright terms: Public domain W3C validator