Metamath Proof Explorer


Theorem rrx2plord

Description: The lexicographical ordering for points in the two dimensional Euclidean plane: a point is less than another point iff its first coordinate is less than the first coordinate of the other point, or the first coordinates of both points are equal and the second coordinate of the first point is less than the second coordinate of the other point: <. a , b >. <_ <. x , y >. iff ( a < x \/ ( a = x /\ b <_ y ) ) . (Contributed by AV, 12-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 rrx2plord.o 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
2 df-br ( 𝑋 𝑂 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑂 )
3 1 eleq2i ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑂 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } )
4 2 3 bitri ( 𝑋 𝑂 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } )
5 fveq1 ( 𝑥 = 𝑋 → ( 𝑥 ‘ 1 ) = ( 𝑋 ‘ 1 ) )
6 fveq1 ( 𝑦 = 𝑌 → ( 𝑦 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
7 5 6 breqan12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ↔ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) )
8 5 6 eqeqan12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ↔ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
9 fveq1 ( 𝑥 = 𝑋 → ( 𝑥 ‘ 2 ) = ( 𝑋 ‘ 2 ) )
10 fveq1 ( 𝑦 = 𝑌 → ( 𝑦 ‘ 2 ) = ( 𝑌 ‘ 2 ) )
11 9 10 breqan12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
12 8 11 anbi12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) )
13 7 12 orbi12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
14 13 opelopab2a ( ( 𝑋𝑅𝑌𝑅 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝑅𝑦𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
15 4 14 syl5bb ( ( 𝑋𝑅𝑌𝑅 ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )