Theorem ltex

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

	Ref	Expression
Assertion	ltex	$$⊢<\in \mathrm{V}$$

Proof

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