Metamath Proof Explorer

Theorem rrx2plord1

Description: The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point if its first coordinate is less than the first coordinate of the other point. (Contributed by AV, 12-Mar-2023)

		Ref	Expression
	Hypothesis	rrx2plord.o	$⊢ O = \{⟨x, y⟩ \| ((x \in R \land y \in R) \land (x (0) < y (0) \lor (x (0) = y (0) \land x (1) < y (1))))\}$
	Assertion	rrx2plord1	$⊢ (X \in R \land Y \in R \land X (0) < Y (0)) \to X O Y$

Proof

Step	Hyp	Ref	Expression
1		rrx2plord.o	$⊢ O = \{⟨x, y⟩ \| ((x \in R \land y \in R) \land (x (0) < y (0) \lor (x (0) = y (0) \land x (1) < y (1))))\}$
2		simp3	$⊢ (X \in R \land Y \in R \land X (0) < Y (0)) \to X (0) < Y (0)$
3	2	orcd	$⊢ (X \in R \land Y \in R \land X (0) < Y (0)) \to (X (0) < Y (0) \lor (X (0) = Y (0) \land X (1) < Y (1)))$
4	1	rrx2plord	$⊢ (X \in R \land Y \in R) \to (X O Y \leftrightarrow (X (0) < Y (0) \lor (X (0) = Y (0) \land X (1) < Y (1))))$
5	4	3adant3	$⊢ (X \in R \land Y \in R \land X (0) < Y (0)) \to (X O Y \leftrightarrow (X (0) < Y (0) \lor (X (0) = Y (0) \land X (1) < Y (1))))$
6	3 5	mpbird	$⊢ (X \in R \land Y \in R \land X (0) < Y (0)) \to X O Y$