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

Metamath Proof Explorer

Theorem ltrelre

Description: 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltrelre	$⊢ <_{ℝ} \subseteq ℝ^{2}$

Step	Hyp	Ref	Expression
1		df-lt	$⊢ <_{ℝ} = \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))\}$
2		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in ℝ \land y \in ℝ) \land \exists z \exists w ((x = ⟨z, 0_{𝑹}⟩ \land y = ⟨w, 0_{𝑹}⟩) \land z <_{𝑹} w))\} \subseteq ℝ^{2}$
3	1 2	eqsstri	$⊢ <_{ℝ} \subseteq ℝ^{2}$