Theorem ltrelsr

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

	Ref	Expression
Assertion	ltrelsr	$$⊢{<}_{𝑹}\subseteq 𝑹\times 𝑹$$

Proof

Step	Hyp	Ref	Expression
1		df-ltr	$$⊢{<}_{𝑹}=\left\{⟨x,y⟩|\left(\left(x\in 𝑹\wedge y\in 𝑹\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=\left[⟨z,w⟩\right]{~}_{𝑹}\wedge y=\left[⟨v,u⟩\right]{~}_{𝑹}\right)\wedge \left(z{+}_{𝑷}u\right){<}_{𝑷}\left(w{+}_{𝑷}v\right)\right)\right)\right\}$$
2		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in 𝑹\wedge y\in 𝑹\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=\left[⟨z,w⟩\right]{~}_{𝑹}\wedge y=\left[⟨v,u⟩\right]{~}_{𝑹}\right)\wedge \left(z{+}_{𝑷}u\right){<}_{𝑷}\left(w{+}_{𝑷}v\right)\right)\right)\right\}\subseteq 𝑹\times 𝑹$$
3	1 2	eqsstri	$$⊢{<}_{𝑹}\subseteq 𝑹\times 𝑹$$