Theorem ltrelpr

Description: Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	ltrelpr	$$⊢{<}_{𝑷}\subseteq 𝑷\times 𝑷$$

Proof

Step	Hyp	Ref	Expression
1		df-ltp	$$⊢{<}_{𝑷}=\left\{⟨x,y⟩|\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge x\subset y\right)\right\}$$
2		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in 𝑷\wedge y\in 𝑷\right)\wedge x\subset y\right)\right\}\subseteq 𝑷\times 𝑷$$
3	1 2	eqsstri	$$⊢{<}_{𝑷}\subseteq 𝑷\times 𝑷$$