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 𝑤 ) ) }