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 (1) < y (1) \lor (x (1) = y (1) \land x (2) < y (2))))\}$
	Assertion	rrx2plord1	$⊢ (X \in R \land Y \in R \land X (1) < Y (1)) \to X O Y$

Proof

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