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

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

Metamath Proof Explorer

Theorem rrx2plord2

Proof