Metamath Proof Explorer

Theorem rrx2plordso

Description: The lexicographical ordering for points in the two dimensional Euclidean plane is a strict total ordering. (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	rrx2plordso	$⊢ O Or R$

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		ltso	$⊢ < Or ℝ$
4		eqid	$⊢ \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} = \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}$
5	4	soxp	$⊢ (< Or ℝ \land < Or ℝ) \to \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} Or ℝ^{2}$
6	3 3 5	mp2an	$⊢ \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} Or ℝ^{2}$
7		eqid	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\})$
8	1 2 7 4	rrx2plordisom	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}, O} (ℝ^{2}, R)$
9		isoso	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}, O} (ℝ^{2}, R) \to (\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} Or ℝ^{2} \leftrightarrow O Or R)$
10	8 9	ax-mp	$⊢ \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} Or ℝ^{2} \leftrightarrow O Or R$
11	6 10	mpbi	$⊢ O Or R$