![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrx2plord | Structured version Visualization version GIF version |
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: 〈𝑎, 𝑏〉 ≤ 〈𝑥, 𝑦〉 iff (𝑎 < 𝑥 ∨ (𝑎 = 𝑥 ∧ 𝑏 ≤ 𝑦)). (Contributed by AV, 12-Mar-2023.) |
Ref | Expression |
---|---|
rrx2plord.o | ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} |
Ref | Expression |
---|---|
rrx2plord | ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝑂𝑌 ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 5106 | . . 3 ⊢ (𝑋𝑂𝑌 ↔ 〈𝑋, 𝑌〉 ∈ 𝑂) | |
2 | rrx2plord.o | . . . 4 ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} | |
3 | 2 | eleq2i 2829 | . . 3 ⊢ (〈𝑋, 𝑌〉 ∈ 𝑂 ↔ 〈𝑋, 𝑌〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))}) |
4 | 1, 3 | bitri 274 | . 2 ⊢ (𝑋𝑂𝑌 ↔ 〈𝑋, 𝑌〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))}) |
5 | fveq1 6841 | . . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥‘1) = (𝑋‘1)) | |
6 | fveq1 6841 | . . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦‘1) = (𝑌‘1)) | |
7 | 5, 6 | breqan12d 5121 | . . . 4 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑥‘1) < (𝑦‘1) ↔ (𝑋‘1) < (𝑌‘1))) |
8 | 5, 6 | eqeqan12d 2750 | . . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑥‘1) = (𝑦‘1) ↔ (𝑋‘1) = (𝑌‘1))) |
9 | fveq1 6841 | . . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥‘2) = (𝑋‘2)) | |
10 | fveq1 6841 | . . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑦‘2) = (𝑌‘2)) | |
11 | 9, 10 | breqan12d 5121 | . . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → ((𝑥‘2) < (𝑦‘2) ↔ (𝑋‘2) < (𝑌‘2))) |
12 | 8, 11 | anbi12d 631 | . . . 4 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2)) ↔ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2)))) |
13 | 7, 12 | orbi12d 917 | . . 3 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))) ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) |
14 | 13 | opelopab2a 5492 | . 2 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (〈𝑋, 𝑌〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) |
15 | 4, 14 | bitrid 282 | 1 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝑂𝑌 ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 〈cop 4592 class class class wbr 5105 {copab 5167 ‘cfv 6496 1c1 11052 < clt 11189 2c2 12208 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-iota 6448 df-fv 6504 |
This theorem is referenced by: rrx2plord1 46797 rrx2plord2 46798 rrx2plordisom 46799 |
Copyright terms: Public domain | W3C validator |