Definition df-ltp

Description: Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c , 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.)

	Ref	Expression
Assertion	df-ltp	|- . | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltp	|-
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4		cnp	|- P.
5	3 4	wcel	|- x e. P.
6	2	cv	|- y
7	6 4	wcel	|- y e. P.
8	5 7	wa	|- ( x e. P. /\ y e. P. )
9	3 6	wpss	|- x C. y
10	8 9	wa	|- ( ( x e. P. /\ y e. P. ) /\ x C. y )
11	10 1 2	copab	|- { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }
12	0 11	wceq	|- . | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }