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$$

Proof

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