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	⊢ <P = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝑥 ⊊ 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltp	⊢ <P
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cnp	⊢ P
5	3 4	wcel	⊢ 𝑥 ∈ P
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ P
8	5 7	wa	⊢ ( 𝑥 ∈ P ∧ 𝑦 ∈ P )
9	3 6	wpss	⊢ 𝑥 ⊊ 𝑦
10	8 9	wa	⊢ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝑥 ⊊ 𝑦 )
11	10 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝑥 ⊊ 𝑦 ) }
12	0 11	wceq	⊢ <P = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ 𝑥 ⊊ 𝑦 ) }