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=\left\{⟨x,y⟩|\left(\left(x\in R\wedge y\in R\right)\wedge \left(x\left(1\right)<y\left(1\right)\vee \left(x\left(1\right)=y\left(1\right)\wedge x\left(2\right)<y\left(2\right)\right)\right)\right)\right\}$$
	rrx2plord2.r	$$⊢R={ℝ}^{\left\{1,2\right\}}$$
Assertion	rrx2plordso	$$⊢O\mathrm{Or}R$$

Proof

Step	Hyp	Ref	Expression
1		rrx2plord.o	$$⊢O=\left\{⟨x,y⟩|\left(\left(x\in R\wedge y\in R\right)\wedge \left(x\left(1\right)<y\left(1\right)\vee \left(x\left(1\right)=y\left(1\right)\wedge x\left(2\right)<y\left(2\right)\right)\right)\right)\right\}$$
2		rrx2plord2.r	$$⊢R={ℝ}^{\left\{1,2\right\}}$$
3		ltso	$$⊢<\mathrm{Or}ℝ$$
4		eqid	$$⊢\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\}$$
5	4	soxp	$$⊢\left(<\mathrm{Or}ℝ\wedge <\mathrm{Or}ℝ\right)\to \left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\}\mathrm{Or}{ℝ}^2$$
6	3 3 5	mp2an	$$⊢\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\}\mathrm{Or}{ℝ}^2$$
7		eqid	$$⊢\left(x\in ℝ,y\in ℝ⟼\left\{⟨1,x⟩,⟨2,y⟩\right\}\right)=\left(x\in ℝ,y\in ℝ⟼\left\{⟨1,x⟩,⟨2,y⟩\right\}\right)$$
8	1 2 7 4	rrx2plordisom	$$⊢\left(x\in ℝ,y\in ℝ⟼\left\{⟨1,x⟩,⟨2,y⟩\right\}\right){Isom}_{\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\},O}\left({ℝ}^2,R\right)$$
9		isoso	$$⊢\left(x\in ℝ,y\in ℝ⟼\left\{⟨1,x⟩,⟨2,y⟩\right\}\right){Isom}_{\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\},O}\left({ℝ}^2,R\right)\to \left(\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\}\mathrm{Or}{ℝ}^2\leftrightarrow O\mathrm{Or}R\right)$$
10	8 9	ax-mp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in {ℝ}^2\wedge y\in {ℝ}^2\right)\wedge \left(1^{st}\left(x\right)<1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)<2^{nd}\left(y\right)\right)\right)\right)\right\}\mathrm{Or}{ℝ}^2\leftrightarrow O\mathrm{Or}R$$
11	6 10	mpbi	$$⊢O\mathrm{Or}R$$