Step | Hyp | Ref
| Expression |
1 | | 2z 12209 |
. . . 4
⊢ 2 ∈
ℤ |
2 | | uzid 12453 |
. . . 4
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ 2 ∈
(ℤ≥‘2) |
4 | | istrkg.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
5 | | istrkg.d |
. . . 4
⊢ − =
(dist‘𝐺) |
6 | | istrkg.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
7 | 4, 5, 6 | istrkgld 26550 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 2 ∈
(ℤ≥‘2)) → (𝐺DimTarskiG≥2 ↔
∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
8 | 3, 7 | mpan2 691 |
. 2
⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥2 ↔
∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
9 | | r19.41v 3260 |
. . . . 5
⊢
(∃𝑥 ∈
𝑃 (∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ∧ 𝑓:(1..^2)–1-1→𝑃) ↔ (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ∧ 𝑓:(1..^2)–1-1→𝑃)) |
10 | | ancom 464 |
. . . . . 6
⊢
((∃𝑦 ∈
𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ∧ 𝑓:(1..^2)–1-1→𝑃) ↔ (𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
11 | 10 | rexbii 3170 |
. . . . 5
⊢
(∃𝑥 ∈
𝑃 (∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ∧ 𝑓:(1..^2)–1-1→𝑃) ↔ ∃𝑥 ∈ 𝑃 (𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
12 | | ancom 464 |
. . . . 5
⊢
((∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ∧ 𝑓:(1..^2)–1-1→𝑃) ↔ (𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
13 | 9, 11, 12 | 3bitr3ri 305 |
. . . 4
⊢ ((𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑥 ∈ 𝑃 (𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
14 | 13 | exbii 1855 |
. . 3
⊢
(∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑓∃𝑥 ∈ 𝑃 (𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
15 | | rexcom4 3172 |
. . 3
⊢
(∃𝑥 ∈
𝑃 ∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑓∃𝑥 ∈ 𝑃 (𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
16 | | simpr 488 |
. . . . . . . . . 10
⊢
((∀𝑗 ∈
(2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
17 | 16 | reximi 3166 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
18 | 17 | reximi 3166 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
19 | 18 | adantl 485 |
. . . . . . 7
⊢ ((𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) → ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
20 | 19 | exlimiv 1938 |
. . . . . 6
⊢
(∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) → ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
21 | 20 | adantl 485 |
. . . . 5
⊢ ((𝑥 ∈ 𝑃 ∧ ∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) → ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
22 | | 1ex 10829 |
. . . . . . . . . 10
⊢ 1 ∈
V |
23 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
24 | 22, 23 | f1osn 6700 |
. . . . . . . . 9
⊢ {〈1,
𝑥〉}:{1}–1-1-onto→{𝑥} |
25 | | f1of1 6660 |
. . . . . . . . 9
⊢
({〈1, 𝑥〉}:{1}–1-1-onto→{𝑥} → {〈1, 𝑥〉}:{1}–1-1→{𝑥}) |
26 | 24, 25 | mp1i 13 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑃 → {〈1, 𝑥〉}:{1}–1-1→{𝑥}) |
27 | | snssi 4721 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑃 → {𝑥} ⊆ 𝑃) |
28 | | f1ss 6621 |
. . . . . . . 8
⊢
(({〈1, 𝑥〉}:{1}–1-1→{𝑥} ∧ {𝑥} ⊆ 𝑃) → {〈1, 𝑥〉}:{1}–1-1→𝑃) |
29 | 26, 27, 28 | syl2anc 587 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑃 → {〈1, 𝑥〉}:{1}–1-1→𝑃) |
30 | | fzo12sn 13325 |
. . . . . . . . . . . 12
⊢ (1..^2) =
{1} |
31 | 30 | mpteq1i 5145 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1..^2) ↦ 𝑥) = (𝑗 ∈ {1} ↦ 𝑥) |
32 | | fmptsn 6982 |
. . . . . . . . . . . 12
⊢ ((1
∈ V ∧ 𝑥 ∈ V)
→ {〈1, 𝑥〉} =
(𝑗 ∈ {1} ↦ 𝑥)) |
33 | 22, 23, 32 | mp2an 692 |
. . . . . . . . . . 11
⊢ {〈1,
𝑥〉} = (𝑗 ∈ {1} ↦ 𝑥) |
34 | 31, 33 | eqtr4i 2768 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1..^2) ↦ 𝑥) = {〈1, 𝑥〉} |
35 | 34 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (𝑗 ∈ (1..^2)
↦ 𝑥) = {〈1,
𝑥〉}) |
36 | 30 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (1..^2) = {1}) |
37 | | eqidd 2738 |
. . . . . . . . 9
⊢ (⊤
→ 𝑃 = 𝑃) |
38 | 35, 36, 37 | f1eq123d 6653 |
. . . . . . . 8
⊢ (⊤
→ ((𝑗 ∈ (1..^2)
↦ 𝑥):(1..^2)–1-1→𝑃 ↔ {〈1, 𝑥〉}:{1}–1-1→𝑃)) |
39 | 38 | mptru 1550 |
. . . . . . 7
⊢ ((𝑗 ∈ (1..^2) ↦ 𝑥):(1..^2)–1-1→𝑃 ↔ {〈1, 𝑥〉}:{1}–1-1→𝑃) |
40 | 29, 39 | sylibr 237 |
. . . . . 6
⊢ (𝑥 ∈ 𝑃 → (𝑗 ∈ (1..^2) ↦ 𝑥):(1..^2)–1-1→𝑃) |
41 | | ral0 4424 |
. . . . . . . . . 10
⊢
∀𝑗 ∈
∅ ((((𝑗 ∈
(1..^2) ↦ 𝑥)‘1)
−
𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) |
42 | | fzo0 13266 |
. . . . . . . . . . 11
⊢ (2..^2) =
∅ |
43 | 42 | raleqi 3323 |
. . . . . . . . . 10
⊢
(∀𝑗 ∈
(2..^2)((((𝑗 ∈ (1..^2)
↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ↔ ∀𝑗 ∈ ∅ ((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧))) |
44 | 41, 43 | mpbir 234 |
. . . . . . . . 9
⊢
∀𝑗 ∈
(2..^2)((((𝑗 ∈ (1..^2)
↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) |
45 | 44 | jctl 527 |
. . . . . . . 8
⊢ (¬
(𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) → (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |
46 | 45 | reximi 3166 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) → ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |
47 | 46 | reximi 3166 |
. . . . . 6
⊢
(∃𝑦 ∈
𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) → ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |
48 | | ovex 7246 |
. . . . . . . 8
⊢ (1..^2)
∈ V |
49 | 48 | mptex 7039 |
. . . . . . 7
⊢ (𝑗 ∈ (1..^2) ↦ 𝑥) ∈ V |
50 | | f1eq1 6610 |
. . . . . . . 8
⊢ (𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) → (𝑓:(1..^2)–1-1→𝑃 ↔ (𝑗 ∈ (1..^2) ↦ 𝑥):(1..^2)–1-1→𝑃)) |
51 | | nfmpt1 5153 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝑗 ∈ (1..^2) ↦ 𝑥) |
52 | 51 | nfeq2 2921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) |
53 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃) |
54 | 52, 53 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) |
55 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → 𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥)) |
56 | 55 | fveq1d 6719 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → (𝑓‘1) = ((𝑗 ∈ (1..^2) ↦ 𝑥)‘1)) |
57 | 56 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((𝑓‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥)) |
58 | 55 | fveq1d 6719 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → (𝑓‘𝑗) = ((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗)) |
59 | 58 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((𝑓‘𝑗) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥)) |
60 | 57, 59 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → (((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ↔ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥))) |
61 | 56 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((𝑓‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦)) |
62 | 58 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((𝑓‘𝑗) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦)) |
63 | 61, 62 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → (((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ↔ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦))) |
64 | 56 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((𝑓‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧)) |
65 | 58 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((𝑓‘𝑗) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) |
66 | 64, 65 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → (((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧) ↔ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧))) |
67 | 60, 63, 66 | 3anbi123d 1438 |
. . . . . . . . . . 11
⊢ (((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) ∧ 𝑗 ∈ (2..^2)) → ((((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ ((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)))) |
68 | 54, 67 | ralbida 3153 |
. . . . . . . . . 10
⊢ ((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ↔ ∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)))) |
69 | 68 | anbi1d 633 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → ((∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
70 | 69 | 2rexbidva 3218 |
. . . . . . . 8
⊢ (𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) → (∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
71 | 50, 70 | anbi12d 634 |
. . . . . . 7
⊢ (𝑓 = (𝑗 ∈ (1..^2) ↦ 𝑥) → ((𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ((𝑗 ∈ (1..^2) ↦ 𝑥):(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))) |
72 | 49, 71 | spcev 3521 |
. . . . . 6
⊢ (((𝑗 ∈ (1..^2) ↦ 𝑥):(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)((((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑥) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑥) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑦) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑦) ∧ (((𝑗 ∈ (1..^2) ↦ 𝑥)‘1) − 𝑧) = (((𝑗 ∈ (1..^2) ↦ 𝑥)‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) → ∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
73 | 40, 47, 72 | syl2an 599 |
. . . . 5
⊢ ((𝑥 ∈ 𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))) |
74 | 21, 73 | impbida 801 |
. . . 4
⊢ (𝑥 ∈ 𝑃 → (∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |
75 | 74 | rexbiia 3169 |
. . 3
⊢
(∃𝑥 ∈
𝑃 ∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
76 | 14, 15, 75 | 3bitr2i 302 |
. 2
⊢
(∃𝑓(𝑓:(1..^2)–1-1→𝑃 ∧ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (∀𝑗 ∈ (2..^2)(((𝑓‘1) − 𝑥) = ((𝑓‘𝑗) − 𝑥) ∧ ((𝑓‘1) − 𝑦) = ((𝑓‘𝑗) − 𝑦) ∧ ((𝑓‘1) − 𝑧) = ((𝑓‘𝑗) − 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) |
77 | 8, 76 | bitrdi 290 |
1
⊢ (𝐺 ∈ 𝑉 → (𝐺DimTarskiG≥2 ↔
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) |