Step | Hyp | Ref
| Expression |
1 | | tgbtwnconn.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | eqid 2818 |
. . . 4
⊢
(dist‘𝐺) =
(dist‘𝐺) |
3 | | tgbtwnconn.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
4 | | tgbtwnconn.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐺 ∈ TarskiG) |
6 | | tgbtwnconn.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐵 ∈ 𝑃) |
8 | | tgbtwnconn.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
9 | 8 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐴 ∈ 𝑃) |
10 | | tgbtwnconn.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
11 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐶 ∈ 𝑃) |
12 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) →
(♯‘𝑃) =
1) |
13 | 1, 2, 3, 5, 7, 9, 11, 12 | tgldim0itv 26217 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐵 ∈ (𝐴𝐼𝐶)) |
14 | 13 | orcd 869 |
. 2
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) |
15 | 4 | ad3antrrr 726 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐺 ∈ TarskiG) |
16 | | simplr 765 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ∈ 𝑃) |
17 | 8 | ad3antrrr 726 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ 𝑃) |
18 | 6 | ad3antrrr 726 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ 𝑃) |
19 | 10 | ad3antrrr 726 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ 𝑃) |
20 | | simprr 769 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ≠ 𝑝) |
21 | 20 | necomd 3068 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝑝 ≠ 𝐴) |
22 | | tgbtwnconn.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
23 | 22 | ad3antrrr 726 |
. . . . . 6
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐷 ∈ 𝑃) |
24 | | tgbtwnconn3.1 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐷)) |
25 | 24 | ad3antrrr 726 |
. . . . . 6
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐵 ∈ (𝐴𝐼𝐷)) |
26 | | simprl 767 |
. . . . . . 7
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ (𝐷𝐼𝑝)) |
27 | 1, 2, 3, 15, 23, 17, 16, 26 | tgbtwncom 26201 |
. . . . . 6
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ (𝑝𝐼𝐷)) |
28 | 1, 2, 3, 15, 18, 17, 16, 23, 25, 27 | tgbtwnintr 26206 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ (𝐵𝐼𝑝)) |
29 | 1, 2, 3, 15, 18, 17, 16, 28 | tgbtwncom 26201 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ (𝑝𝐼𝐵)) |
30 | | tgbtwnconn3.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝐷)) |
31 | 30 | ad3antrrr 726 |
. . . . . . 7
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ (𝐴𝐼𝐷)) |
32 | 1, 2, 3, 15, 17, 19, 23, 31 | tgbtwncom 26201 |
. . . . . 6
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐶 ∈ (𝐷𝐼𝐴)) |
33 | 1, 2, 3, 15, 23, 19, 17, 16, 32, 26 | tgbtwnexch3 26207 |
. . . . 5
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ (𝐶𝐼𝑝)) |
34 | 1, 2, 3, 15, 19, 17, 16, 33 | tgbtwncom 26201 |
. . . 4
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → 𝐴 ∈ (𝑝𝐼𝐶)) |
35 | 1, 3, 15, 16, 17, 18, 19, 21, 29, 34 | tgbtwnconn2 26289 |
. . 3
⊢ ((((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑝 ∈ 𝑃) ∧ (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) |
36 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐺 ∈ TarskiG) |
37 | 22 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐷 ∈ 𝑃) |
38 | 8 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 𝐴 ∈ 𝑃) |
39 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → 2 ≤
(♯‘𝑃)) |
40 | 1, 2, 3, 36, 37, 38, 39 | tgbtwndiff 26219 |
. . 3
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → ∃𝑝 ∈ 𝑃 (𝐴 ∈ (𝐷𝐼𝑝) ∧ 𝐴 ≠ 𝑝)) |
41 | 35, 40 | r19.29a 3286 |
. 2
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) |
42 | 1, 8 | tgldimor 26215 |
. 2
⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤
(♯‘𝑃))) |
43 | 14, 41, 42 | mpjaodan 952 |
1
⊢ (𝜑 → (𝐵 ∈ (𝐴𝐼𝐶) ∨ 𝐶 ∈ (𝐴𝐼𝐵))) |