Proof of Theorem hltr
| Step | Hyp | Ref
| Expression |
| 1 | | ishlg.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | ishlg.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
| 3 | | ishlg.k |
. . 3
⊢ 𝐾 = (hlG‘𝐺) |
| 4 | | ishlg.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 5 | | ishlg.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 6 | | hltr.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 7 | | hlln.1 |
. . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 8 | | hltr.1 |
. . 3
⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐵) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | hlne1 28613 |
. 2
⊢ (𝜑 → 𝐴 ≠ 𝐷) |
| 10 | | ishlg.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 11 | | hltr.2 |
. . 3
⊢ (𝜑 → 𝐵(𝐾‘𝐷)𝐶) |
| 12 | 1, 2, 3, 5, 10, 6,
7, 11 | hlne2 28614 |
. 2
⊢ (𝜑 → 𝐶 ≠ 𝐷) |
| 13 | | eqid 2737 |
. . . . . 6
⊢
(dist‘𝐺) =
(dist‘𝐺) |
| 14 | 7 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐺 ∈ TarskiG) |
| 15 | 6 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐷 ∈ 𝑃) |
| 16 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐴 ∈ 𝑃) |
| 17 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐵 ∈ 𝑃) |
| 18 | 10 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐶 ∈ 𝑃) |
| 19 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐴 ∈ (𝐷𝐼𝐵)) |
| 20 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐵 ∈ (𝐷𝐼𝐶)) |
| 21 | 1, 13, 2, 14, 15, 16, 17, 18, 19, 20 | tgbtwnexch 28506 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐴 ∈ (𝐷𝐼𝐶)) |
| 22 | 21 | orcd 874 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 23 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 24 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐷 ∈ 𝑃) |
| 25 | 4 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 26 | 10 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐶 ∈ 𝑃) |
| 27 | 5 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 28 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐴 ∈ (𝐷𝐼𝐵)) |
| 29 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐶 ∈ (𝐷𝐼𝐵)) |
| 30 | 1, 2, 23, 24, 25, 26, 27, 28, 29 | tgbtwnconn3 28585 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 31 | 1, 2, 3, 5, 10, 6,
7 | ishlg 28610 |
. . . . . . 7
⊢ (𝜑 → (𝐵(𝐾‘𝐷)𝐶 ↔ (𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ∧ (𝐵 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐵))))) |
| 32 | 11, 31 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ∧ (𝐵 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐵)))) |
| 33 | 32 | simp3d 1145 |
. . . . 5
⊢ (𝜑 → (𝐵 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐵))) |
| 34 | 33 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) → (𝐵 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐵))) |
| 35 | 22, 30, 34 | mpjaodan 961 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐷𝐼𝐵)) → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 36 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐺 ∈ TarskiG) |
| 37 | 6 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐷 ∈ 𝑃) |
| 38 | 5 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐵 ∈ 𝑃) |
| 39 | 4 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐴 ∈ 𝑃) |
| 40 | 10 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐶 ∈ 𝑃) |
| 41 | 32 | simp1d 1143 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≠ 𝐷) |
| 42 | 41 | necomd 2996 |
. . . . . 6
⊢ (𝜑 → 𝐷 ≠ 𝐵) |
| 43 | 42 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐷 ≠ 𝐵) |
| 44 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐵 ∈ (𝐷𝐼𝐴)) |
| 45 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → 𝐵 ∈ (𝐷𝐼𝐶)) |
| 46 | 1, 2, 36, 37, 38, 39, 40, 43, 44, 45 | tgbtwnconn1 28583 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐵 ∈ (𝐷𝐼𝐶)) → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 47 | 7 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 48 | 6 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐷 ∈ 𝑃) |
| 49 | 10 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐶 ∈ 𝑃) |
| 50 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 51 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 52 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐶 ∈ (𝐷𝐼𝐵)) |
| 53 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐵 ∈ (𝐷𝐼𝐴)) |
| 54 | 1, 13, 2, 47, 48, 49, 50, 51, 52, 53 | tgbtwnexch 28506 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → 𝐶 ∈ (𝐷𝐼𝐴)) |
| 55 | 54 | olcd 875 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) ∧ 𝐶 ∈ (𝐷𝐼𝐵)) → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 56 | 33 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) → (𝐵 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐵))) |
| 57 | 46, 55, 56 | mpjaodan 961 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐷𝐼𝐴)) → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 58 | 1, 2, 3, 4, 5, 6, 7 | ishlg 28610 |
. . . . 5
⊢ (𝜑 → (𝐴(𝐾‘𝐷)𝐵 ↔ (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ (𝐴 ∈ (𝐷𝐼𝐵) ∨ 𝐵 ∈ (𝐷𝐼𝐴))))) |
| 59 | 8, 58 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ (𝐴 ∈ (𝐷𝐼𝐵) ∨ 𝐵 ∈ (𝐷𝐼𝐴)))) |
| 60 | 59 | simp3d 1145 |
. . 3
⊢ (𝜑 → (𝐴 ∈ (𝐷𝐼𝐵) ∨ 𝐵 ∈ (𝐷𝐼𝐴))) |
| 61 | 35, 57, 60 | mpjaodan 961 |
. 2
⊢ (𝜑 → (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))) |
| 62 | 1, 2, 3, 4, 10, 6,
7 | ishlg 28610 |
. 2
⊢ (𝜑 → (𝐴(𝐾‘𝐷)𝐶 ↔ (𝐴 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ∧ (𝐴 ∈ (𝐷𝐼𝐶) ∨ 𝐶 ∈ (𝐷𝐼𝐴))))) |
| 63 | 9, 12, 61, 62 | mpbir3and 1343 |
1
⊢ (𝜑 → 𝐴(𝐾‘𝐷)𝐶) |