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

Definition df-reap 7639
 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 7646 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 7651). (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 7638 . 2 #
2 vx . . . . . . 7
32cv 1258 . . . . . 6
4 cr 6945 . . . . . 6
53, 4wcel 1409 . . . . 5
6 vy . . . . . . 7
76cv 1258 . . . . . 6
87, 4wcel 1409 . . . . 5
95, 8wa 101 . . . 4
10 clt 7118 . . . . . 6
113, 7, 10wbr 3791 . . . . 5
127, 3, 10wbr 3791 . . . . 5
1311, 12wo 639 . . . 4
149, 13wa 101 . . 3
1514, 2, 6copab 3844 . 2
161, 15wceq 1259 1 #
 Colors of variables: wff set class This definition is referenced by:  reapval  7640
 Copyright terms: Public domain W3C validator