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 ∈ P ∧ y ∈ 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 ∈ P
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ P
9	5, 8	wa 196	. . . 4 wff (x ∈ P ∧ y ∈ P)
10	3, 7	wpss 1488	. . . 4 wff x ⊂ y
11	9, 10	wa 196	. . 3 wff ((x ∈ P ∧ y ∈ P) ∧ x ⊂ y)
12	11, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣((x ∈ P ∧ y ∈ P) ∧ x ⊂ y)}
13	1, 12	wceq 1091	1 wff <P = {⟨x, y⟩∣((x ∈ P ∧ y ∈ P) ∧ x ⊂ y)}

This definition is referenced by:  ltrelpr 3895  ltprord 3928

metamath.org