rrx2plord2

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

	Ref	Expression
Hypotheses	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))))\}$
	rrx2plord2.r	$⊢ R = ℝ^{\{1, 2\}}$
Assertion	rrx2plord2	$⊢ (X \in R \land Y \in R \land X (1) = Y (1)) \to (X O Y \leftrightarrow X (2) < Y (2))$

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		rrx2plord2.r	$⊢ R = ℝ^{\{1, 2\}}$
3	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))))$
4	3	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))))$
5		eqid	$⊢ \{1, 2\} = \{1, 2\}$
6	5 2	rrx2pxel	$⊢ X \in R \to X (1) \in ℝ$
7	6	adantr	$⊢ (X \in R \land Y \in R) \to X (1) \in ℝ$
8		ltne	$⊢ (X (1) \in ℝ \land X (1) < Y (1)) \to Y (1) \neq X (1)$
9	8	necomd	$⊢ (X (1) \in ℝ \land X (1) < Y (1)) \to X (1) \neq Y (1)$
10	7 9	sylan	$⊢ ((X \in R \land Y \in R) \land X (1) < Y (1)) \to X (1) \neq Y (1)$
11	10	ex	$⊢ (X \in R \land Y \in R) \to (X (1) < Y (1) \to X (1) \neq Y (1))$
12		eqneqall	$⊢ X (1) = Y (1) \to (X (1) \neq Y (1) \to X (2) < Y (2))$
13	11 12	syl9	$⊢ (X \in R \land Y \in R) \to (X (1) = Y (1) \to (X (1) < Y (1) \to X (2) < Y (2)))$
14	13	3impia	$⊢ (X \in R \land Y \in R \land X (1) = Y (1)) \to (X (1) < Y (1) \to X (2) < Y (2))$
15	14	com12	$⊢ X (1) < Y (1) \to ((X \in R \land Y \in R \land X (1) = Y (1)) \to X (2) < Y (2))$
16		simpr	$⊢ (X (1) = Y (1) \land X (2) < Y (2)) \to X (2) < Y (2)$
17	16	a1d	$⊢ (X (1) = Y (1) \land X (2) < Y (2)) \to ((X \in R \land Y \in R \land X (1) = Y (1)) \to X (2) < Y (2))$
18	15 17	jaoi	$⊢ (X (1) < Y (1) \lor (X (1) = Y (1) \land X (2) < Y (2))) \to ((X \in R \land Y \in R \land X (1) = Y (1)) \to X (2) < Y (2))$
19	18	com12	$⊢ (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))) \to X (2) < Y (2))$
20		olc	$⊢ (X (1) = Y (1) \land X (2) < Y (2)) \to (X (1) < Y (1) \lor (X (1) = Y (1) \land X (2) < Y (2)))$
21	20	ex	$⊢ X (1) = Y (1) \to (X (2) < Y (2) \to (X (1) < Y (1) \lor (X (1) = Y (1) \land X (2) < Y (2))))$
22	21	3ad2ant3	$⊢ (X \in R \land Y \in R \land X (1) = Y (1)) \to (X (2) < Y (2) \to (X (1) < Y (1) \lor (X (1) = Y (1) \land X (2) < Y (2))))$
23	19 22	impbid	$⊢ (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))) \leftrightarrow X (2) < Y (2))$
24	4 23	bitrd	$⊢ (X \in R \land Y \in R \land X (1) = Y (1)) \to (X O Y \leftrightarrow X (2) < Y (2))$

Metamath Proof Explorer

Theorem rrx2plord2

Proof