Definition df-ltp 3884

Description: Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. From Proposition 9-3.2 of [Gleason] p. 122.

Assertion

Ref	Expression
df-ltp	|- <P = {<.x, y>. | ((x e. P. /\ y e. P.) /\ x (. y)}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-ltp

Step	Hyp	Ref	Expression
1		cltp 3783	. 2 class <P
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cnp 3779	. . . . . 6 class P.
5	3, 4	wcel 1092	. . . . 5 wff x e. P.
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. P.
9	5, 8	wa 196	. . . 4 wff (x e. P. /\ y e. P.)
10	3, 7	wpss 1488	. . . 4 wff x (. y
11	9, 10	wa 196	. . 3 wff ((x e. P. /\ y e. P.) /\ x (. y)
12	11, 2, 6	copab 2055	. 2 class {<.x, y>. | ((x e. P. /\ y e. P.) /\ x (. y)}
13	1, 12	wceq 1091	1 wff <P = {<.x, y>. | ((x e. P. /\ y e. P.) /\ x (. y)}

This definition is referenced by:  ltrelpr 3895  ltprord 3928

metamath.org