Theorem rrx2plord1

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

	Ref	Expression
Hypothesis	rrx2plord.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
Assertion	rrx2plord1	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → 𝑋 𝑂 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		rrx2plord.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
2		simp3	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) )
3	2	orcd	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) )
4	1	rrx2plord	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
5	4	3adant3	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
6	3 5	mpbird	⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → 𝑋 𝑂 𝑌 )