Theorem ltex

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

	Ref	Expression
Assertion	ltex	⊢ < ∈ V

Proof

Step	Hyp	Ref	Expression
1		xrex	⊢ ℝ* ∈ V
2	1 1	xpex	⊢ ( ℝ* × ℝ* ) ∈ V
3		ltrelxr	⊢ < ⊆ ( ℝ* × ℝ* )
4	2 3	ssexi	⊢ < ∈ V