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 𝑹$

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

Metamath Proof Explorer