Step | Hyp | Ref
| Expression |
1 | | cstrkgld 27949 |
. 2
class
DimTarskiGβ₯ |
2 | | c1 11113 |
. . . . . . . . . 10
class
1 |
3 | | vn |
. . . . . . . . . . 11
setvar π |
4 | 3 | cv 1538 |
. . . . . . . . . 10
class π |
5 | | cfzo 13631 |
. . . . . . . . . 10
class
..^ |
6 | 2, 4, 5 | co 7411 |
. . . . . . . . 9
class
(1..^π) |
7 | | vp |
. . . . . . . . . 10
setvar π |
8 | 7 | cv 1538 |
. . . . . . . . 9
class π |
9 | | vf |
. . . . . . . . . 10
setvar π |
10 | 9 | cv 1538 |
. . . . . . . . 9
class π |
11 | 6, 8, 10 | wf1 6539 |
. . . . . . . 8
wff π:(1..^π)β1-1βπ |
12 | 2, 10 | cfv 6542 |
. . . . . . . . . . . . . . . 16
class (πβ1) |
13 | | vx |
. . . . . . . . . . . . . . . . 17
setvar π₯ |
14 | 13 | cv 1538 |
. . . . . . . . . . . . . . . 16
class π₯ |
15 | | vd |
. . . . . . . . . . . . . . . . 17
setvar π |
16 | 15 | cv 1538 |
. . . . . . . . . . . . . . . 16
class π |
17 | 12, 14, 16 | co 7411 |
. . . . . . . . . . . . . . 15
class ((πβ1)ππ₯) |
18 | | vj |
. . . . . . . . . . . . . . . . . 18
setvar π |
19 | 18 | cv 1538 |
. . . . . . . . . . . . . . . . 17
class π |
20 | 19, 10 | cfv 6542 |
. . . . . . . . . . . . . . . 16
class (πβπ) |
21 | 20, 14, 16 | co 7411 |
. . . . . . . . . . . . . . 15
class ((πβπ)ππ₯) |
22 | 17, 21 | wceq 1539 |
. . . . . . . . . . . . . 14
wff ((πβ1)ππ₯) = ((πβπ)ππ₯) |
23 | | vy |
. . . . . . . . . . . . . . . . 17
setvar π¦ |
24 | 23 | cv 1538 |
. . . . . . . . . . . . . . . 16
class π¦ |
25 | 12, 24, 16 | co 7411 |
. . . . . . . . . . . . . . 15
class ((πβ1)ππ¦) |
26 | 20, 24, 16 | co 7411 |
. . . . . . . . . . . . . . 15
class ((πβπ)ππ¦) |
27 | 25, 26 | wceq 1539 |
. . . . . . . . . . . . . 14
wff ((πβ1)ππ¦) = ((πβπ)ππ¦) |
28 | | vz |
. . . . . . . . . . . . . . . . 17
setvar π§ |
29 | 28 | cv 1538 |
. . . . . . . . . . . . . . . 16
class π§ |
30 | 12, 29, 16 | co 7411 |
. . . . . . . . . . . . . . 15
class ((πβ1)ππ§) |
31 | 20, 29, 16 | co 7411 |
. . . . . . . . . . . . . . 15
class ((πβπ)ππ§) |
32 | 30, 31 | wceq 1539 |
. . . . . . . . . . . . . 14
wff ((πβ1)ππ§) = ((πβπ)ππ§) |
33 | 22, 27, 32 | w3a 1085 |
. . . . . . . . . . . . 13
wff (((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) |
34 | | c2 12271 |
. . . . . . . . . . . . . 14
class
2 |
35 | 34, 4, 5 | co 7411 |
. . . . . . . . . . . . 13
class
(2..^π) |
36 | 33, 18, 35 | wral 3059 |
. . . . . . . . . . . 12
wff
βπ β
(2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) |
37 | | vi |
. . . . . . . . . . . . . . . . 17
setvar π |
38 | 37 | cv 1538 |
. . . . . . . . . . . . . . . 16
class π |
39 | 14, 24, 38 | co 7411 |
. . . . . . . . . . . . . . 15
class (π₯ππ¦) |
40 | 29, 39 | wcel 2104 |
. . . . . . . . . . . . . 14
wff π§ β (π₯ππ¦) |
41 | 29, 24, 38 | co 7411 |
. . . . . . . . . . . . . . 15
class (π§ππ¦) |
42 | 14, 41 | wcel 2104 |
. . . . . . . . . . . . . 14
wff π₯ β (π§ππ¦) |
43 | 14, 29, 38 | co 7411 |
. . . . . . . . . . . . . . 15
class (π₯ππ§) |
44 | 24, 43 | wcel 2104 |
. . . . . . . . . . . . . 14
wff π¦ β (π₯ππ§) |
45 | 40, 42, 44 | w3o 1084 |
. . . . . . . . . . . . 13
wff (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
46 | 45 | wn 3 |
. . . . . . . . . . . 12
wff Β¬
(π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
47 | 36, 46 | wa 394 |
. . . . . . . . . . 11
wff
(βπ β
(2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
48 | 47, 28, 8 | wrex 3068 |
. . . . . . . . . 10
wff
βπ§ β
π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
49 | 48, 23, 8 | wrex 3068 |
. . . . . . . . 9
wff
βπ¦ β
π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
50 | 49, 13, 8 | wrex 3068 |
. . . . . . . 8
wff
βπ₯ β
π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
51 | 11, 50 | wa 394 |
. . . . . . 7
wff (π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
52 | 51, 9 | wex 1779 |
. . . . . 6
wff
βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
53 | | vg |
. . . . . . . 8
setvar π |
54 | 53 | cv 1538 |
. . . . . . 7
class π |
55 | | citv 27951 |
. . . . . . 7
class
Itv |
56 | 54, 55 | cfv 6542 |
. . . . . 6
class
(Itvβπ) |
57 | 52, 37, 56 | wsbc 3776 |
. . . . 5
wff
[(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
58 | | cds 17210 |
. . . . . 6
class
dist |
59 | 54, 58 | cfv 6542 |
. . . . 5
class
(distβπ) |
60 | 57, 15, 59 | wsbc 3776 |
. . . 4
wff
[(distβπ) / π][(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
61 | | cbs 17148 |
. . . . 5
class
Base |
62 | 54, 61 | cfv 6542 |
. . . 4
class
(Baseβπ) |
63 | 60, 7, 62 | wsbc 3776 |
. . 3
wff
[(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
64 | 63, 53, 3 | copab 5209 |
. 2
class
{β¨π, πβ© β£
[(Baseβπ) /
π][(distβπ) / π][(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))))} |
65 | 1, 64 | wceq 1539 |
1
wff
DimTarskiGβ₯ = {β¨π, πβ© β£ [(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π]βπ(π:(1..^π)β1-1βπ β§ βπ₯ β π βπ¦ β π βπ§ β π (βπ β (2..^π)(((πβ1)ππ₯) = ((πβπ)ππ₯) β§ ((πβ1)ππ¦) = ((πβπ)ππ¦) β§ ((πβ1)ππ§) = ((πβπ)ππ§)) β§ Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))))} |