Step | Hyp | Ref
| Expression |
1 | | cstrkg2d 33974 |
. 2
class
TarskiG2D |
2 | | vz |
. . . . . . . . . . . . . 14
setvar π§ |
3 | 2 | cv 1538 |
. . . . . . . . . . . . 13
class π§ |
4 | | vx |
. . . . . . . . . . . . . . 15
setvar π₯ |
5 | 4 | cv 1538 |
. . . . . . . . . . . . . 14
class π₯ |
6 | | vy |
. . . . . . . . . . . . . . 15
setvar π¦ |
7 | 6 | cv 1538 |
. . . . . . . . . . . . . 14
class π¦ |
8 | | vi |
. . . . . . . . . . . . . . 15
setvar π |
9 | 8 | cv 1538 |
. . . . . . . . . . . . . 14
class π |
10 | 5, 7, 9 | co 7411 |
. . . . . . . . . . . . 13
class (π₯ππ¦) |
11 | 3, 10 | wcel 2104 |
. . . . . . . . . . . 12
wff π§ β (π₯ππ¦) |
12 | 3, 7, 9 | co 7411 |
. . . . . . . . . . . . 13
class (π§ππ¦) |
13 | 5, 12 | wcel 2104 |
. . . . . . . . . . . 12
wff π₯ β (π§ππ¦) |
14 | 5, 3, 9 | co 7411 |
. . . . . . . . . . . . 13
class (π₯ππ§) |
15 | 7, 14 | wcel 2104 |
. . . . . . . . . . . 12
wff π¦ β (π₯ππ§) |
16 | 11, 13, 15 | w3o 1084 |
. . . . . . . . . . 11
wff (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
17 | 16 | wn 3 |
. . . . . . . . . 10
wff Β¬
(π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
18 | | vp |
. . . . . . . . . . 11
setvar π |
19 | 18 | cv 1538 |
. . . . . . . . . 10
class π |
20 | 17, 2, 19 | wrex 3068 |
. . . . . . . . 9
wff
βπ§ β
π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
21 | 20, 6, 19 | wrex 3068 |
. . . . . . . 8
wff
βπ¦ β
π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
22 | 21, 4, 19 | wrex 3068 |
. . . . . . 7
wff
βπ₯ β
π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) |
23 | | vu |
. . . . . . . . . . . . . . . . . 18
setvar π’ |
24 | 23 | cv 1538 |
. . . . . . . . . . . . . . . . 17
class π’ |
25 | | vd |
. . . . . . . . . . . . . . . . . 18
setvar π |
26 | 25 | cv 1538 |
. . . . . . . . . . . . . . . . 17
class π |
27 | 5, 24, 26 | co 7411 |
. . . . . . . . . . . . . . . 16
class (π₯ππ’) |
28 | | vv |
. . . . . . . . . . . . . . . . . 18
setvar π£ |
29 | 28 | cv 1538 |
. . . . . . . . . . . . . . . . 17
class π£ |
30 | 5, 29, 26 | co 7411 |
. . . . . . . . . . . . . . . 16
class (π₯ππ£) |
31 | 27, 30 | wceq 1539 |
. . . . . . . . . . . . . . 15
wff (π₯ππ’) = (π₯ππ£) |
32 | 7, 24, 26 | co 7411 |
. . . . . . . . . . . . . . . 16
class (π¦ππ’) |
33 | 7, 29, 26 | co 7411 |
. . . . . . . . . . . . . . . 16
class (π¦ππ£) |
34 | 32, 33 | wceq 1539 |
. . . . . . . . . . . . . . 15
wff (π¦ππ’) = (π¦ππ£) |
35 | 3, 24, 26 | co 7411 |
. . . . . . . . . . . . . . . 16
class (π§ππ’) |
36 | 3, 29, 26 | co 7411 |
. . . . . . . . . . . . . . . 16
class (π§ππ£) |
37 | 35, 36 | wceq 1539 |
. . . . . . . . . . . . . . 15
wff (π§ππ’) = (π§ππ£) |
38 | 31, 34, 37 | w3a 1085 |
. . . . . . . . . . . . . 14
wff ((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) |
39 | 24, 29 | wne 2938 |
. . . . . . . . . . . . . 14
wff π’ β π£ |
40 | 38, 39 | wa 394 |
. . . . . . . . . . . . 13
wff (((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) |
41 | 40, 16 | wi 4 |
. . . . . . . . . . . 12
wff ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
42 | 41, 28, 19 | wral 3059 |
. . . . . . . . . . 11
wff
βπ£ β
π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
43 | 42, 23, 19 | wral 3059 |
. . . . . . . . . 10
wff
βπ’ β
π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
44 | 43, 2, 19 | wral 3059 |
. . . . . . . . 9
wff
βπ§ β
π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
45 | 44, 6, 19 | wral 3059 |
. . . . . . . 8
wff
βπ¦ β
π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
46 | 45, 4, 19 | wral 3059 |
. . . . . . 7
wff
βπ₯ β
π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))) |
47 | 22, 46 | wa 394 |
. . . . . 6
wff
(βπ₯ β
π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
48 | | vf |
. . . . . . . 8
setvar π |
49 | 48 | cv 1538 |
. . . . . . 7
class π |
50 | | citv 27951 |
. . . . . . 7
class
Itv |
51 | 49, 50 | cfv 6542 |
. . . . . 6
class
(Itvβπ) |
52 | 47, 8, 51 | wsbc 3776 |
. . . . 5
wff
[(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
53 | | cds 17210 |
. . . . . 6
class
dist |
54 | 49, 53 | cfv 6542 |
. . . . 5
class
(distβπ) |
55 | 52, 25, 54 | wsbc 3776 |
. . . 4
wff
[(distβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
56 | | cbs 17148 |
. . . . 5
class
Base |
57 | 49, 56 | cfv 6542 |
. . . 4
class
(Baseβπ) |
58 | 55, 18, 57 | wsbc 3776 |
. . 3
wff
[(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)))) |
59 | 58, 48 | cab 2707 |
. 2
class {π β£
[(Baseβπ) /
π][(distβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))))} |
60 | 1, 59 | wceq 1539 |
1
wff
TarskiG2D = {π β£ [(Baseβπ) / π][(distβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π βπ§ β π Β¬ (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§)) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((((π₯ππ’) = (π₯ππ£) β§ (π¦ππ’) = (π¦ππ£) β§ (π§ππ’) = (π§ππ£)) β§ π’ β π£) β (π§ β (π₯ππ¦) β¨ π₯ β (π§ππ¦) β¨ π¦ β (π₯ππ§))))} |