Step | Hyp | Ref
| Expression |
1 | | 3z 12351 |
. . . 4
⊢ 3 ∈
ℤ |
2 | | 2re 12045 |
. . . . 5
⊢ 2 ∈
ℝ |
3 | | 3re 12051 |
. . . . 5
⊢ 3 ∈
ℝ |
4 | | 2lt3 12143 |
. . . . 5
⊢ 2 <
3 |
5 | 2, 3, 4 | ltleii 11096 |
. . . 4
⊢ 2 ≤
3 |
6 | | 2z 12350 |
. . . . 5
⊢ 2 ∈
ℤ |
7 | 6 | eluz1i 12588 |
. . . 4
⊢ (3 ∈
(ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤
3)) |
8 | 1, 5, 7 | mpbir2an 708 |
. . 3
⊢ 3 ∈
(ℤ≥‘2) |
9 | | istrkg.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
10 | | istrkg.d |
. . . 4
⊢ − =
(dist‘𝐺) |
11 | | istrkg.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
12 | 9, 10, 11 | istrkgld 26818 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 3 ∈
(ℤ≥‘2)) → (𝐺DimTarskiG≥3 ↔
∃𝑓(𝑓:(1..^3)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
13 | 8, 12 | mpan2 688 |
. 2
⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥3 ↔
∃𝑓(𝑓:(1..^3)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
14 | | fzo13pr 13469 |
. . . . . 6
⊢ (1..^3) =
{1, 2} |
15 | | f1eq2 6668 |
. . . . . 6
⊢ ((1..^3)
= {1, 2} → (𝑓:(1..^3)–1-1→𝑃 ↔ 𝑓:{1, 2}–1-1→𝑃)) |
16 | 14, 15 | ax-mp 5 |
. . . . 5
⊢ (𝑓:(1..^3)–1-1→𝑃 ↔ 𝑓:{1, 2}–1-1→𝑃) |
17 | 16 | anbi1i 624 |
. . . 4
⊢ ((𝑓:(1..^3)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ (𝑓:{1, 2}–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
18 | 17 | exbii 1850 |
. . 3
⊢
(∃𝑓(𝑓:(1..^3)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑓(𝑓:{1, 2}–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
19 | 18 | a1i 11 |
. 2
⊢ (𝐺 ∈ 𝑉 → (∃𝑓(𝑓:(1..^3)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑓(𝑓:{1, 2}–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
20 | | 1z 12348 |
. . . 4
⊢ 1 ∈
ℤ |
21 | | 1ne2 12179 |
. . . 4
⊢ 1 ≠
2 |
22 | | oveq1 7284 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑓‘1) → (𝑢 − 𝑥) = ((𝑓‘1) − 𝑥)) |
23 | 22 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑢 = (𝑓‘1) → ((𝑢 − 𝑥) = (𝑣 − 𝑥) ↔ ((𝑓‘1) − 𝑥) = (𝑣 − 𝑥))) |
24 | | oveq1 7284 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑓‘1) → (𝑢 − 𝑦) = ((𝑓‘1) − 𝑦)) |
25 | 24 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑢 = (𝑓‘1) → ((𝑢 − 𝑦) = (𝑣 − 𝑦) ↔ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦))) |
26 | | oveq1 7284 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑓‘1) → (𝑢 − 𝑧) = ((𝑓‘1) − 𝑧)) |
27 | 26 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑢 = (𝑓‘1) → ((𝑢 − 𝑧) = (𝑣 − 𝑧) ↔ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧))) |
28 | 23, 25, 27 | 3anbi123d 1435 |
. . . . . . . 8
⊢ (𝑢 = (𝑓‘1) → (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ↔ (((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)))) |
29 | 28 | anbi1d 630 |
. . . . . . 7
⊢ (𝑢 = (𝑓‘1) → ((((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
30 | 29 | rexbidv 3225 |
. . . . . 6
⊢ (𝑢 = (𝑓‘1) → (∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑧 ∈ 𝑃 ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
31 | 30 | 2rexbidv 3228 |
. . . . 5
⊢ (𝑢 = (𝑓‘1) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
32 | | oveq1 7284 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑓‘2) → (𝑣 − 𝑥) = ((𝑓‘2) − 𝑥)) |
33 | 32 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑓‘2) → (((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ↔ ((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥))) |
34 | | oveq1 7284 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑓‘2) → (𝑣 − 𝑦) = ((𝑓‘2) − 𝑦)) |
35 | 34 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑓‘2) → (((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ↔ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦))) |
36 | | oveq1 7284 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑓‘2) → (𝑣 − 𝑧) = ((𝑓‘2) − 𝑧)) |
37 | 36 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑓‘2) → (((𝑓‘1) − 𝑧) = (𝑣 − 𝑧) ↔ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧))) |
38 | 33, 35, 37 | 3anbi123d 1435 |
. . . . . . . . 9
⊢ (𝑣 = (𝑓‘2) → ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ↔ (((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧)))) |
39 | | 2p1e3 12113 |
. . . . . . . . . . . . 13
⊢ (2 + 1) =
3 |
40 | 39 | oveq2i 7288 |
. . . . . . . . . . . 12
⊢ (2..^(2 +
1)) = (2..^3) |
41 | | fzosn 13456 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℤ → (2..^(2 + 1)) = {2}) |
42 | 6, 41 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (2..^(2 +
1)) = {2} |
43 | 40, 42 | eqtr3i 2768 |
. . . . . . . . . . 11
⊢ (2..^3) =
{2} |
44 | 43 | raleqi 3345 |
. . . . . . . . . 10
⊢
(∀𝑗 ∈
(2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ ∀𝑗 ∈ {2} (((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧))) |
45 | | fveq2 6776 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 2 → (𝑓‘𝑗) = (𝑓‘2)) |
46 | 45 | oveq1d 7292 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 2 → ((𝑓‘𝑗) − 𝑥) = ((𝑓‘2) − 𝑥)) |
47 | 46 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 2 → (((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ↔ ((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥))) |
48 | 45 | oveq1d 7292 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 2 → ((𝑓‘𝑗) − 𝑦) = ((𝑓‘2) − 𝑦)) |
49 | 48 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 2 → (((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ↔ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦))) |
50 | 45 | oveq1d 7292 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 2 → ((𝑓‘𝑗) − 𝑧) = ((𝑓‘2) − 𝑧)) |
51 | 50 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 2 → (((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧) ↔ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧))) |
52 | 47, 49, 51 | 3anbi123d 1435 |
. . . . . . . . . . . 12
⊢ (𝑗 = 2 → ((((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ (((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧)))) |
53 | 52 | ralsng 4611 |
. . . . . . . . . . 11
⊢ (2 ∈
ℤ → (∀𝑗
∈ {2} (((𝑓‘1)
−
𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ (((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧)))) |
54 | 6, 53 | ax-mp 5 |
. . . . . . . . . 10
⊢
(∀𝑗 ∈
{2} (((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ (((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧))) |
55 | 44, 54 | bitri 274 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
(2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ (((𝑓‘1) − 𝑥) = ((𝑓‘2) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘2) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘2) − 𝑧))) |
56 | 38, 55 | bitr4di 289 |
. . . . . . . 8
⊢ (𝑣 = (𝑓‘2) → ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ↔ ∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)))) |
57 | 56 | anbi1d 630 |
. . . . . . 7
⊢ (𝑣 = (𝑓‘2) → (((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
58 | 57 | rexbidv 3225 |
. . . . . 6
⊢ (𝑣 = (𝑓‘2) → (∃𝑧 ∈ 𝑃 ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
59 | 58 | 2rexbidv 3228 |
. . . . 5
⊢ (𝑣 = (𝑓‘2) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ((((𝑓‘1) − 𝑥) = (𝑣 − 𝑥) ∧ ((𝑓‘1) − 𝑦) = (𝑣 − 𝑦) ∧ ((𝑓‘1) − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
60 | 31, 59 | f1prex 7158 |
. . . 4
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ≠ 2) → (∃𝑓(𝑓:{1, 2}–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 (𝑢 ≠ 𝑣 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
61 | 20, 6, 21, 60 | mp3an 1460 |
. . 3
⊢
(∃𝑓(𝑓:{1, 2}–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 (𝑢 ≠ 𝑣 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
62 | 61 | a1i 11 |
. 2
⊢ (𝐺 ∈ 𝑉 → (∃𝑓(𝑓:{1, 2}–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^3)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 (𝑢 ≠ 𝑣 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
63 | 13, 19, 62 | 3bitrd 305 |
1
⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥3 ↔
∃𝑢 ∈ 𝑃 ∃𝑣 ∈ 𝑃 (𝑢 ≠ 𝑣 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (((𝑢 − 𝑥) = (𝑣 − 𝑥) ∧ (𝑢 − 𝑦) = (𝑣 − 𝑦) ∧ (𝑢 − 𝑧) = (𝑣 − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |