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	$$⊢{<}_{𝑷}=\left\{⟨x,y⟩|\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge x\subset y\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltp	$$class{<}_{𝑷}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4		cnp	$$class𝑷$$
5	3 4	wcel	$$wffx\in 𝑷$$
6	2	cv	$$setvary$$
7	6 4	wcel	$$wffy\in 𝑷$$
8	5 7	wa	$$wff\left(x\in 𝑷\wedge y\in 𝑷\right)$$
9	3 6	wpss	$$wffx\subset y$$
10	8 9	wa	$$wff\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge x\subset y\right)$$
11	10 1 2	copab	$$class\left\{⟨x,y⟩|\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge x\subset y\right)\right\}$$
12	0 11	wceq	$$wff{<}_{𝑷}=\left\{⟨x,y⟩|\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge x\subset y\right)\right\}$$