Step | Hyp | Ref
| Expression |
1 | | cstrkgb 27947 |
. 2
class
TarskiGB |
2 | | vy |
. . . . . . . . . . 11
setvar π¦ |
3 | 2 | cv 1538 |
. . . . . . . . . 10
class π¦ |
4 | | vx |
. . . . . . . . . . . 12
setvar π₯ |
5 | 4 | cv 1538 |
. . . . . . . . . . 11
class π₯ |
6 | | vi |
. . . . . . . . . . . 12
setvar π |
7 | 6 | cv 1538 |
. . . . . . . . . . 11
class π |
8 | 5, 5, 7 | co 7411 |
. . . . . . . . . 10
class (π₯ππ₯) |
9 | 3, 8 | wcel 2104 |
. . . . . . . . 9
wff π¦ β (π₯ππ₯) |
10 | 4, 2 | weq 1964 |
. . . . . . . . 9
wff π₯ = π¦ |
11 | 9, 10 | wi 4 |
. . . . . . . 8
wff (π¦ β (π₯ππ₯) β π₯ = π¦) |
12 | | vp |
. . . . . . . . 9
setvar π |
13 | 12 | cv 1538 |
. . . . . . . 8
class π |
14 | 11, 2, 13 | wral 3059 |
. . . . . . 7
wff
βπ¦ β
π (π¦ β (π₯ππ₯) β π₯ = π¦) |
15 | 14, 4, 13 | wral 3059 |
. . . . . 6
wff
βπ₯ β
π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) |
16 | | vu |
. . . . . . . . . . . . . . 15
setvar π’ |
17 | 16 | cv 1538 |
. . . . . . . . . . . . . 14
class π’ |
18 | | vz |
. . . . . . . . . . . . . . . 16
setvar π§ |
19 | 18 | cv 1538 |
. . . . . . . . . . . . . . 15
class π§ |
20 | 5, 19, 7 | co 7411 |
. . . . . . . . . . . . . 14
class (π₯ππ§) |
21 | 17, 20 | wcel 2104 |
. . . . . . . . . . . . 13
wff π’ β (π₯ππ§) |
22 | | vv |
. . . . . . . . . . . . . . 15
setvar π£ |
23 | 22 | cv 1538 |
. . . . . . . . . . . . . 14
class π£ |
24 | 3, 19, 7 | co 7411 |
. . . . . . . . . . . . . 14
class (π¦ππ§) |
25 | 23, 24 | wcel 2104 |
. . . . . . . . . . . . 13
wff π£ β (π¦ππ§) |
26 | 21, 25 | wa 394 |
. . . . . . . . . . . 12
wff (π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) |
27 | | va |
. . . . . . . . . . . . . . . 16
setvar π |
28 | 27 | cv 1538 |
. . . . . . . . . . . . . . 15
class π |
29 | 17, 3, 7 | co 7411 |
. . . . . . . . . . . . . . 15
class (π’ππ¦) |
30 | 28, 29 | wcel 2104 |
. . . . . . . . . . . . . 14
wff π β (π’ππ¦) |
31 | 23, 5, 7 | co 7411 |
. . . . . . . . . . . . . . 15
class (π£ππ₯) |
32 | 28, 31 | wcel 2104 |
. . . . . . . . . . . . . 14
wff π β (π£ππ₯) |
33 | 30, 32 | wa 394 |
. . . . . . . . . . . . 13
wff (π β (π’ππ¦) β§ π β (π£ππ₯)) |
34 | 33, 27, 13 | wrex 3068 |
. . . . . . . . . . . 12
wff
βπ β
π (π β (π’ππ¦) β§ π β (π£ππ₯)) |
35 | 26, 34 | wi 4 |
. . . . . . . . . . 11
wff ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) |
36 | 35, 22, 13 | wral 3059 |
. . . . . . . . . 10
wff
βπ£ β
π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) |
37 | 36, 16, 13 | wral 3059 |
. . . . . . . . 9
wff
βπ’ β
π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) |
38 | 37, 18, 13 | wral 3059 |
. . . . . . . 8
wff
βπ§ β
π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) |
39 | 38, 2, 13 | wral 3059 |
. . . . . . 7
wff
βπ¦ β
π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) |
40 | 39, 4, 13 | wral 3059 |
. . . . . 6
wff
βπ₯ β
π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) |
41 | 28, 3, 7 | co 7411 |
. . . . . . . . . . . . 13
class (πππ¦) |
42 | 5, 41 | wcel 2104 |
. . . . . . . . . . . 12
wff π₯ β (πππ¦) |
43 | | vt |
. . . . . . . . . . . . 13
setvar π‘ |
44 | 43 | cv 1538 |
. . . . . . . . . . . 12
class π‘ |
45 | 42, 2, 44 | wral 3059 |
. . . . . . . . . . 11
wff
βπ¦ β
π‘ π₯ β (πππ¦) |
46 | | vs |
. . . . . . . . . . . 12
setvar π |
47 | 46 | cv 1538 |
. . . . . . . . . . 11
class π |
48 | 45, 4, 47 | wral 3059 |
. . . . . . . . . 10
wff
βπ₯ β
π βπ¦ β π‘ π₯ β (πππ¦) |
49 | 48, 27, 13 | wrex 3068 |
. . . . . . . . 9
wff
βπ β
π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) |
50 | | vb |
. . . . . . . . . . . . . 14
setvar π |
51 | 50 | cv 1538 |
. . . . . . . . . . . . 13
class π |
52 | 5, 3, 7 | co 7411 |
. . . . . . . . . . . . 13
class (π₯ππ¦) |
53 | 51, 52 | wcel 2104 |
. . . . . . . . . . . 12
wff π β (π₯ππ¦) |
54 | 53, 2, 44 | wral 3059 |
. . . . . . . . . . 11
wff
βπ¦ β
π‘ π β (π₯ππ¦) |
55 | 54, 4, 47 | wral 3059 |
. . . . . . . . . 10
wff
βπ₯ β
π βπ¦ β π‘ π β (π₯ππ¦) |
56 | 55, 50, 13 | wrex 3068 |
. . . . . . . . 9
wff
βπ β
π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦) |
57 | 49, 56 | wi 4 |
. . . . . . . 8
wff
(βπ β
π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)) |
58 | 13 | cpw 4601 |
. . . . . . . 8
class π«
π |
59 | 57, 43, 58 | wral 3059 |
. . . . . . 7
wff
βπ‘ β
π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)) |
60 | 59, 46, 58 | wral 3059 |
. . . . . 6
wff
βπ β
π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)) |
61 | 15, 40, 60 | w3a 1085 |
. . . . 5
wff
(βπ₯ β
π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦))) |
62 | | vf |
. . . . . . 7
setvar π |
63 | 62 | cv 1538 |
. . . . . 6
class π |
64 | | citv 27951 |
. . . . . 6
class
Itv |
65 | 63, 64 | cfv 6542 |
. . . . 5
class
(Itvβπ) |
66 | 61, 6, 65 | wsbc 3776 |
. . . 4
wff
[(Itvβπ) / π](βπ₯ β π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦))) |
67 | | cbs 17148 |
. . . . 5
class
Base |
68 | 63, 67 | cfv 6542 |
. . . 4
class
(Baseβπ) |
69 | 66, 12, 68 | wsbc 3776 |
. . 3
wff
[(Baseβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦))) |
70 | 69, 62 | cab 2707 |
. 2
class {π β£
[(Baseβπ) /
π][(Itvβπ) / π](βπ₯ β π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)))} |
71 | 1, 70 | wceq 1539 |
1
wff
TarskiGB = {π β£ [(Baseβπ) / π][(Itvβπ) / π](βπ₯ β π βπ¦ β π (π¦ β (π₯ππ₯) β π₯ = π¦) β§ βπ₯ β π βπ¦ β π βπ§ β π βπ’ β π βπ£ β π ((π’ β (π₯ππ§) β§ π£ β (π¦ππ§)) β βπ β π (π β (π’ππ¦) β§ π β (π£ππ₯))) β§ βπ β π« πβπ‘ β π« π(βπ β π βπ₯ β π βπ¦ β π‘ π₯ β (πππ¦) β βπ β π βπ₯ β π βπ¦ β π‘ π β (π₯ππ¦)))} |