Definition df-reap 8532

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 8539 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 8544). (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 8531	. 2 class #ℝ
2		vx	. . . . . . 7 setvar x
3	2	cv 1352	. . . . . 6 class x
4		cr 7810	. . . . . 6 class RR
5	3, 4	wcel 2148	. . . . 5 wff x e. RR
6		vy	. . . . . . 7 setvar y
7	6	cv 1352	. . . . . 6 class y
8	7, 4	wcel 2148	. . . . 5 wff y e. RR
9	5, 8	wa 104	. . . 4 wff ( x e. RR /\ y e. RR )
10		clt 7992	. . . . . 6 class <
11	3, 7, 10	wbr 4004	. . . . 5 wff x < y
12	7, 3, 10	wbr 4004	. . . . 5 wff y < x
13	11, 12	wo 708	. . . 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 4064	. 2 class { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
16	1, 15	wceq 1353	1 wff #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }

This definition is referenced by:  reapval  8533