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

Metamath Proof Explorer

Definition df-lt

Description: Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr . (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion df-lt <ℝ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltrr ⊢ <ℝ
1 vx ⊢ 𝑥
2 vy ⊢ 𝑦
3 1 cv ⊢ 𝑥
4 cr ⊢ ℝ
5 3 4 wcel ⊢ 𝑥 ∈ ℝ
6 2 cv ⊢ 𝑦
7 6 4 wcel ⊢ 𝑦 ∈ ℝ
8 5 7 wa ⊢ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ )
9 vz ⊢ 𝑧
10 vw ⊢ 𝑤
11 9 cv ⊢ 𝑧
12 c0r ⊢ 0R
13 11 12 cop ⊢ ⟨ 𝑧 , 0R ⟩
14 3 13 wceq ⊢ 𝑥 = ⟨ 𝑧 , 0R ⟩
15 10 cv ⊢ 𝑤
16 15 12 cop ⊢ ⟨ 𝑤 , 0R ⟩
17 6 16 wceq ⊢ 𝑦 = ⟨ 𝑤 , 0R ⟩
18 14 17 wa ⊢ ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ )
19 cltr ⊢ <R
20 11 15 19 wbr ⊢ 𝑧 <R 𝑤
21 18 20 wa ⊢ ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 )
22 21 10 wex ⊢ ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 )
23 22 9 wex ⊢ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 )
24 8 23 wa ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 ) )
25 24 1 2 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 ) ) }
26 0 25 wceq ⊢ <ℝ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0R ⟩ ) ∧ 𝑧 <R 𝑤 ) ) }