Definition df-ltp 9807

Description: Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9942, and is intended to be used only by the construction. From Proposition 9-3.2 of [Gleason] p. 122. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-ltp

Step	Hyp	Ref	Expression
1		cltp 9685	. 2 class <P
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		cnp 9681	. . . . . 6 class P.
5	3, 4	wcel 1990	. . . . 5 wff x e. P.
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8	7, 4	wcel 1990	. . . . 5 wff y e. P.
9	5, 8	wa 384	. . . 4 wff ( x e. P. /\ y e. P. )
10	3, 7	wpss 3575	. . . 4 wff x C. y
11	9, 10	wa 384	. . 3 wff ( ( x e. P. /\ y e. P. ) /\ x C. y )
12	11, 2, 6	copab 4712	. 2 class { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }
13	1, 12	wceq 1483	1 wff <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }

This definition is referenced by:  ltrelpr  9820  ltprord  9852