Metamath Proof Explorer

Theorem rrx2plord2

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

Ref Expression
Hypotheses rrx2plord.o ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
rrx2plord2.r ⊢ 𝑅 = ( ℝ ↑m { 1 , 2 } )
Assertion rrx2plord2 ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝑂 𝑌 ↔ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 rrx2plord.o ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
2 rrx2plord2.r ⊢ 𝑅 = ( ℝ ↑m { 1 , 2 } )
3 1 rrx2plord ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
4 3 3adant3 ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
5 eqid ⊢ { 1 , 2 } = { 1 , 2 }
6 5 2 rrx2pxel ⊢ ( 𝑋 ∈ 𝑅 → ( 𝑋 ‘ 1 ) ∈ ℝ )
7 6 adantr ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
8 ltne ⊢ ( ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ≠ ( 𝑋 ‘ 1 ) )
9 8 necomd ⊢ ( ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
10 7 9 sylan ⊢ ( ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
11 10 ex ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) )
12 eqneqall ⊢ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
13 11 12 syl9 ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) )
14 13 3impia ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
15 14 com12 ⊢ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
16 simpr ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) )
17 16 a1d ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
18 15 17 jaoi ⊢ ( ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
19 18 com12 ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
20 olc ⊢ ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) )
21 20 ex ⊢ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) → ( ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
22 21 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) )
23 19 22 impbid ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ↔ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )
24 4 23 bitrd ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝑂 𝑌 ↔ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) )