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	$⊢ <_{ℝ} = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltrr	$class <_{ℝ}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cr	$class ℝ$
5	3 4	wcel	$wff x \in ℝ$
6	2	cv	$setvar y$
7	6 4	wcel	$wff y \in ℝ$
8	5 7	wa	$wff (x \in ℝ \land y \in ℝ)$
9		vz	$setvar z$
10		vw	$setvar w$
11	9	cv	$setvar z$
12		c0r	$class 0_{𝑹}$
13	11 12	cop	$class ⟨z, 0_{𝑹}⟩$
14	3 13	wceq	$wff x = ⟨z, 0_{𝑹}⟩$
15	10	cv	$setvar w$
16	15 12	cop	$class ⟨w, 0_{𝑹}⟩$
17	6 16	wceq	$wff y = ⟨w, 0_{𝑹}⟩$
18	14 17	wa	$wff (x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩)$
19		cltr	$class <_{𝑹}$
20	11 15 19	wbr	$wff z <_{𝑹} w$
21	18 20	wa	$wff ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)$
22	21 10	wex	$wff \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)$
23	22 9	wex	$wff \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w)$
24	8 23	wa	$wff ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))$
25	24 1 2	copab	$class \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))\}$
26	0 25	wceq	$wff <_{ℝ} = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))\}$

Metamath Proof Explorer

Definition df-lt

Detailed syntax breakdown