Definition df-reap 8602

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 8609 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 8614). (Contributed by Jim Kingdon, 26-Jan-2020.)

Assertion

Ref	Expression
df-reap	|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-reap

Step	Hyp	Ref	Expression
1		creap 8601	. 2 class #ℝ
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4		cr 7878	. . . . . 6 class RR
5	3, 4	wcel 2167	. . . . 5 wff x e. RR
6		vy	. . . . . . 7 setvar y
7	6	cv 1363	. . . . . 6 class y
8	7, 4	wcel 2167	. . . . 5 wff y e. RR
9	5, 8	wa 104	. . . 4 wff ( x e. RR /\ y e. RR )
10		clt 8061	. . . . . 6 class <
11	3, 7, 10	wbr 4033	. . . . 5 wff x < y
12	7, 3, 10	wbr 4033	. . . . 5 wff y < x
13	11, 12	wo 709	. . . 4 wff ( x < y \/ y < x )
14	9, 13	wa 104	. . 3 wff ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) )
15	14, 2, 6	copab 4093	. 2 class { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
16	1, 15	wceq 1364	1 wff #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }

This definition is referenced by:  reapval  8603