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

Metamath Proof Explorer

Theorem ltex

Description: The less-than relation is a set. (Contributed by SN, 5-Jun-2025)

		Ref	Expression
	Assertion	ltex	$⊢ < \in V$

Step	Hyp	Ref	Expression
1		xrex	$⊢ ℝ^{*} \in V$
2	1 1	xpex	$⊢ ℝ^{} \times ℝ^{} \in V$
3		ltrelxr	$⊢ < \subseteq ℝ^{} \times ℝ^{}$
4	2 3	ssexi	$⊢ < \in V$