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	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
		rrx2plord2.r	⊢ 𝑅 = ( ℝ ↑_m { 1 , 2 } )
	Assertion	rrx2plordso	⊢ 𝑂 Or 𝑅

Proof

Step	Hyp	Ref	Expression
1		rrx2plord.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
2		rrx2plord2.r	⊢ 𝑅 = ( ℝ ↑_m { 1 , 2 } )
3		ltso	⊢ < Or ℝ
4		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) }
5	4	soxp	⊢ ( ( < Or ℝ ∧ < Or ℝ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } Or ( ℝ × ℝ ) )
6	3 3 5	mp2an	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } Or ( ℝ × ℝ )
7		eqid	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } )
8	1 2 7 4	rrx2plordisom	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )
9		isoso	⊢ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } Or ( ℝ × ℝ ) ↔ 𝑂 Or 𝑅 ) )
10	8 9	ax-mp	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1^st ‘ 𝑥 ) < ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) < ( 2^nd ‘ 𝑦 ) ) ) ) } Or ( ℝ × ℝ ) ↔ 𝑂 Or 𝑅 )
11	6 10	mpbi	⊢ 𝑂 Or 𝑅