Proof of Theorem ltord1
| Step | Hyp | Ref
| Expression |
| 1 | | ltord.1 |
. . 3
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) |
| 2 | | ltord.2 |
. . 3
⊢ (𝑥 = 𝐶 → 𝐴 = 𝑀) |
| 3 | | ltord.3 |
. . 3
⊢ (𝑥 = 𝐷 → 𝐴 = 𝑁) |
| 4 | | ltord.4 |
. . 3
⊢ 𝑆 ⊆
ℝ |
| 5 | | ltord.5 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
| 6 | | ltord.6 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 < 𝑦 → 𝐴 < 𝐵)) |
| 7 | 1, 2, 3, 4, 5, 6 | ltordlem 11788 |
. 2
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 → 𝑀 < 𝑁)) |
| 8 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → (𝑥 = 𝐷 ↔ 𝐶 = 𝐷)) |
| 9 | 2 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → (𝐴 = 𝑁 ↔ 𝑀 = 𝑁)) |
| 10 | 8, 9 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → ((𝑥 = 𝐷 → 𝐴 = 𝑁) ↔ (𝐶 = 𝐷 → 𝑀 = 𝑁))) |
| 11 | 10, 3 | vtoclg 3554 |
. . . . . 6
⊢ (𝐶 ∈ 𝑆 → (𝐶 = 𝐷 → 𝑀 = 𝑁)) |
| 12 | 11 | ad2antrl 728 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 = 𝐷 → 𝑀 = 𝑁)) |
| 13 | 1, 3, 2, 4, 5, 6 | ltordlem 11788 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐷 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → (𝐷 < 𝐶 → 𝑁 < 𝑀)) |
| 14 | 13 | ancom2s 650 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐷 < 𝐶 → 𝑁 < 𝑀)) |
| 15 | 12, 14 | orim12d 967 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ((𝐶 = 𝐷 ∨ 𝐷 < 𝐶) → (𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
| 16 | 15 | con3d 152 |
. . 3
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (¬ (𝑀 = 𝑁 ∨ 𝑁 < 𝑀) → ¬ (𝐶 = 𝐷 ∨ 𝐷 < 𝐶))) |
| 17 | 5 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℝ) |
| 18 | 2 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ)) |
| 19 | 18 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑆 𝐴 ∈ ℝ ∧ 𝐶 ∈ 𝑆) → 𝑀 ∈ ℝ) |
| 20 | 17, 19 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑆) → 𝑀 ∈ ℝ) |
| 21 | 3 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → (𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ)) |
| 22 | 21 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑆 𝐴 ∈ ℝ ∧ 𝐷 ∈ 𝑆) → 𝑁 ∈ ℝ) |
| 23 | 17, 22 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝐷 ∈ 𝑆) → 𝑁 ∈ ℝ) |
| 24 | 20, 23 | anim12dan 619 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
| 25 | | axlttri 11332 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ (𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
| 26 | 24, 25 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝑀 < 𝑁 ↔ ¬ (𝑀 = 𝑁 ∨ 𝑁 < 𝑀))) |
| 27 | 4 | sseli 3979 |
. . . . 5
⊢ (𝐶 ∈ 𝑆 → 𝐶 ∈ ℝ) |
| 28 | 4 | sseli 3979 |
. . . . 5
⊢ (𝐷 ∈ 𝑆 → 𝐷 ∈ ℝ) |
| 29 | | axlttri 11332 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 < 𝐷 ↔ ¬ (𝐶 = 𝐷 ∨ 𝐷 < 𝐶))) |
| 30 | 27, 28, 29 | syl2an 596 |
. . . 4
⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → (𝐶 < 𝐷 ↔ ¬ (𝐶 = 𝐷 ∨ 𝐷 < 𝐶))) |
| 31 | 30 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ ¬ (𝐶 = 𝐷 ∨ 𝐷 < 𝐶))) |
| 32 | 16, 26, 31 | 3imtr4d 294 |
. 2
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝑀 < 𝑁 → 𝐶 < 𝐷)) |
| 33 | 7, 32 | impbid 212 |
1
⊢ ((𝜑 ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐶 < 𝐷 ↔ 𝑀 < 𝑁)) |