Step | Hyp | Ref
| Expression |
1 | | tgdim01.x |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
2 | | tgdim01.y |
. 2
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
3 | | tgdim01.z |
. 2
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
4 | | tgdim01.1 |
. . . 4
⊢ (𝜑 → ¬ 𝐺DimTarskiG≥2) |
5 | | tgdim01.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
6 | | tgdim01.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
7 | | eqid 2610 |
. . . . . 6
⊢
(dist‘𝐺) =
(dist‘𝐺) |
8 | | tgdim01.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
9 | 6, 7, 8 | istrkg2ld 25159 |
. . . . 5
⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥2 ↔
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |
10 | 5, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺DimTarskiG≥2 ↔
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |
11 | 4, 10 | mtbid 313 |
. . 3
⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
12 | | rexnal2 3025 |
. . . . . 6
⊢
(∃𝑦 ∈
𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
13 | 12 | rexbii 3023 |
. . . . 5
⊢
(∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ∃𝑥 ∈ 𝑃 ¬ ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
14 | | rexnal 2978 |
. . . . 5
⊢
(∃𝑥 ∈
𝑃 ¬ ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
15 | 13, 14 | bitri 263 |
. . . 4
⊢
(∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
16 | 15 | con2bii 346 |
. . 3
⊢
(∀𝑥 ∈
𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
17 | 11, 16 | sylibr 223 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
18 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑦) = (𝑋𝐼𝑦)) |
19 | 18 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑦))) |
20 | | eleq1 2676 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑦))) |
21 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧)) |
22 | 21 | eleq2d 2673 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧))) |
23 | 19, 20, 22 | 3orbi123d 1390 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))) |
24 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (𝑋𝐼𝑦) = (𝑋𝐼𝑌)) |
25 | 24 | eleq2d 2673 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑧 ∈ (𝑋𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑌))) |
26 | | oveq2 6557 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (𝑧𝐼𝑦) = (𝑧𝐼𝑌)) |
27 | 26 | eleq2d 2673 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑋 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑌))) |
28 | | eleq1 2676 |
. . . . 5
⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧))) |
29 | 25, 27, 28 | 3orbi123d 1390 |
. . . 4
⊢ (𝑦 = 𝑌 → ((𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))) |
30 | | eleq1 2676 |
. . . . 5
⊢ (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑋𝐼𝑌))) |
31 | | oveq1 6556 |
. . . . . 6
⊢ (𝑧 = 𝑍 → (𝑧𝐼𝑌) = (𝑍𝐼𝑌)) |
32 | 31 | eleq2d 2673 |
. . . . 5
⊢ (𝑧 = 𝑍 → (𝑋 ∈ (𝑧𝐼𝑌) ↔ 𝑋 ∈ (𝑍𝐼𝑌))) |
33 | | oveq2 6557 |
. . . . . 6
⊢ (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍)) |
34 | 33 | eleq2d 2673 |
. . . . 5
⊢ (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍))) |
35 | 30, 32, 34 | 3orbi123d 1390 |
. . . 4
⊢ (𝑧 = 𝑍 → ((𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) |
36 | 23, 29, 35 | rspc3v 3296 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))) |
37 | 36 | imp 444 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) |
38 | 1, 2, 3, 17, 37 | syl31anc 1321 |
1
⊢ (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) |