Definition df-lt 6902

Description: Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)

Assertion

Ref	Expression
df-lt	|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }

Distinct variable group:   x, y, z, w

Detailed syntax breakdown of Definition df-lt

Step	Hyp	Ref	Expression
1		cltrr 6893	. 2 class <RR
2		vx	. . . . . . 7 setvar x
3	2	cv 1242	. . . . . 6 class x
4		cr 6888	. . . . . 6 class RR
5	3, 4	wcel 1393	. . . . 5 wff x e. RR
6		vy	. . . . . . 7 setvar y
7	6	cv 1242	. . . . . 6 class y
8	7, 4	wcel 1393	. . . . 5 wff y e. RR
9	5, 8	wa 97	. . . 4 wff ( x e. RR /\ y e. RR )
10		vz	. . . . . . . . . . 11 setvar z
11	10	cv 1242	. . . . . . . . . 10 class z
12		c0r 6396	. . . . . . . . . 10 class 0R
13	11, 12	cop 3378	. . . . . . . . 9 class <. z , 0R >.
14	3, 13	wceq 1243	. . . . . . . 8 wff x = <. z , 0R >.
15		vw	. . . . . . . . . . 11 setvar w
16	15	cv 1242	. . . . . . . . . 10 class w
17	16, 12	cop 3378	. . . . . . . . 9 class <. w , 0R >.
18	7, 17	wceq 1243	. . . . . . . 8 wff y = <. w , 0R >.
19	14, 18	wa 97	. . . . . . 7 wff ( x = <. z , 0R >. /\ y = <. w , 0R >. )
20		cltr 6401	. . . . . . . 8 class <R
21	11, 16, 20	wbr 3764	. . . . . . 7 wff z <R w
22	19, 21	wa 97	. . . . . 6 wff ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w )
23	22, 15	wex 1381	. . . . 5 wff E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w )
24	23, 10	wex 1381	. . . 4 wff E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w )
25	9, 24	wa 97	. . 3 wff ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) )
26	25, 2, 6	copab 3817	. 2 class { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
27	1, 26	wceq 1243	1 wff <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }

This definition is referenced by:  ltrelre  6909  ltresr  6915