Proof of Theorem rrx2plord2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rrx2plord.o | . . . 4
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} | 
| 2 | 1 | rrx2plord 48646 | . . 3
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋𝑂𝑌 ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) | 
| 3 | 2 | 3adant3 1132 | . 2
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋𝑂𝑌 ↔ ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) | 
| 4 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ {1, 2} =
{1, 2} | 
| 5 |  | rrx2plord2.r | . . . . . . . . . . . 12
⊢ 𝑅 = (ℝ ↑m
{1, 2}) | 
| 6 | 4, 5 | rrx2pxel 48637 | . . . . . . . . . . 11
⊢ (𝑋 ∈ 𝑅 → (𝑋‘1) ∈ ℝ) | 
| 7 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → (𝑋‘1) ∈ ℝ) | 
| 8 |  | ltne 11359 | . . . . . . . . . . 11
⊢ (((𝑋‘1) ∈ ℝ ∧
(𝑋‘1) < (𝑌‘1)) → (𝑌‘1) ≠ (𝑋‘1)) | 
| 9 | 8 | necomd 2995 | . . . . . . . . . 10
⊢ (((𝑋‘1) ∈ ℝ ∧
(𝑋‘1) < (𝑌‘1)) → (𝑋‘1) ≠ (𝑌‘1)) | 
| 10 | 7, 9 | sylan 580 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) ∧ (𝑋‘1) < (𝑌‘1)) → (𝑋‘1) ≠ (𝑌‘1)) | 
| 11 | 10 | ex 412 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → ((𝑋‘1) < (𝑌‘1) → (𝑋‘1) ≠ (𝑌‘1))) | 
| 12 |  | eqneqall 2950 | . . . . . . . 8
⊢ ((𝑋‘1) = (𝑌‘1) → ((𝑋‘1) ≠ (𝑌‘1) → (𝑋‘2) < (𝑌‘2))) | 
| 13 | 11, 12 | syl9 77 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅) → ((𝑋‘1) = (𝑌‘1) → ((𝑋‘1) < (𝑌‘1) → (𝑋‘2) < (𝑌‘2)))) | 
| 14 | 13 | 3impia 1117 | . . . . . 6
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → ((𝑋‘1) < (𝑌‘1) → (𝑋‘2) < (𝑌‘2))) | 
| 15 | 14 | com12 32 | . . . . 5
⊢ ((𝑋‘1) < (𝑌‘1) → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋‘2) < (𝑌‘2))) | 
| 16 |  | simpr 484 | . . . . . 6
⊢ (((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2)) → (𝑋‘2) < (𝑌‘2)) | 
| 17 | 16 | a1d 25 | . . . . 5
⊢ (((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2)) → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋‘2) < (𝑌‘2))) | 
| 18 | 15, 17 | jaoi 857 | . . . 4
⊢ (((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))) → ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋‘2) < (𝑌‘2))) | 
| 19 | 18 | com12 32 | . . 3
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))) → (𝑋‘2) < (𝑌‘2))) | 
| 20 |  | olc 868 | . . . . 5
⊢ (((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2)) → ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2)))) | 
| 21 | 20 | ex 412 | . . . 4
⊢ ((𝑋‘1) = (𝑌‘1) → ((𝑋‘2) < (𝑌‘2) → ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) | 
| 22 | 21 | 3ad2ant3 1135 | . . 3
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → ((𝑋‘2) < (𝑌‘2) → ((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))))) | 
| 23 | 19, 22 | impbid 212 | . 2
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (((𝑋‘1) < (𝑌‘1) ∨ ((𝑋‘1) = (𝑌‘1) ∧ (𝑋‘2) < (𝑌‘2))) ↔ (𝑋‘2) < (𝑌‘2))) | 
| 24 | 3, 23 | bitrd 279 | 1
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ (𝑋‘1) = (𝑌‘1)) → (𝑋𝑂𝑌 ↔ (𝑋‘2) < (𝑌‘2))) |