This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∧ 𝑥 ⊊ 𝑦 ) }