Detailed syntax breakdown of Definition df-trkgb
Step | Hyp | Ref
| Expression |
1 | | cstrkgb 26771 |
. 2
class
TarskiGB |
2 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
3 | 2 | cv 1540 |
. . . . . . . . . 10
class 𝑦 |
4 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
5 | 4 | cv 1540 |
. . . . . . . . . . 11
class 𝑥 |
6 | | vi |
. . . . . . . . . . . 12
setvar 𝑖 |
7 | 6 | cv 1540 |
. . . . . . . . . . 11
class 𝑖 |
8 | 5, 5, 7 | co 7268 |
. . . . . . . . . 10
class (𝑥𝑖𝑥) |
9 | 3, 8 | wcel 2109 |
. . . . . . . . 9
wff 𝑦 ∈ (𝑥𝑖𝑥) |
10 | 4, 2 | weq 1969 |
. . . . . . . . 9
wff 𝑥 = 𝑦 |
11 | 9, 10 | wi 4 |
. . . . . . . 8
wff (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) |
12 | | vp |
. . . . . . . . 9
setvar 𝑝 |
13 | 12 | cv 1540 |
. . . . . . . 8
class 𝑝 |
14 | 11, 2, 13 | wral 3065 |
. . . . . . 7
wff
∀𝑦 ∈
𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) |
15 | 14, 4, 13 | wral 3065 |
. . . . . 6
wff
∀𝑥 ∈
𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) |
16 | | vu |
. . . . . . . . . . . . . . 15
setvar 𝑢 |
17 | 16 | cv 1540 |
. . . . . . . . . . . . . 14
class 𝑢 |
18 | | vz |
. . . . . . . . . . . . . . . 16
setvar 𝑧 |
19 | 18 | cv 1540 |
. . . . . . . . . . . . . . 15
class 𝑧 |
20 | 5, 19, 7 | co 7268 |
. . . . . . . . . . . . . 14
class (𝑥𝑖𝑧) |
21 | 17, 20 | wcel 2109 |
. . . . . . . . . . . . 13
wff 𝑢 ∈ (𝑥𝑖𝑧) |
22 | | vv |
. . . . . . . . . . . . . . 15
setvar 𝑣 |
23 | 22 | cv 1540 |
. . . . . . . . . . . . . 14
class 𝑣 |
24 | 3, 19, 7 | co 7268 |
. . . . . . . . . . . . . 14
class (𝑦𝑖𝑧) |
25 | 23, 24 | wcel 2109 |
. . . . . . . . . . . . 13
wff 𝑣 ∈ (𝑦𝑖𝑧) |
26 | 21, 25 | wa 395 |
. . . . . . . . . . . 12
wff (𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) |
27 | | va |
. . . . . . . . . . . . . . . 16
setvar 𝑎 |
28 | 27 | cv 1540 |
. . . . . . . . . . . . . . 15
class 𝑎 |
29 | 17, 3, 7 | co 7268 |
. . . . . . . . . . . . . . 15
class (𝑢𝑖𝑦) |
30 | 28, 29 | wcel 2109 |
. . . . . . . . . . . . . 14
wff 𝑎 ∈ (𝑢𝑖𝑦) |
31 | 23, 5, 7 | co 7268 |
. . . . . . . . . . . . . . 15
class (𝑣𝑖𝑥) |
32 | 28, 31 | wcel 2109 |
. . . . . . . . . . . . . 14
wff 𝑎 ∈ (𝑣𝑖𝑥) |
33 | 30, 32 | wa 395 |
. . . . . . . . . . . . 13
wff (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)) |
34 | 33, 27, 13 | wrex 3066 |
. . . . . . . . . . . 12
wff
∃𝑎 ∈
𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)) |
35 | 26, 34 | wi 4 |
. . . . . . . . . . 11
wff ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) |
36 | 35, 22, 13 | wral 3065 |
. . . . . . . . . 10
wff
∀𝑣 ∈
𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) |
37 | 36, 16, 13 | wral 3065 |
. . . . . . . . 9
wff
∀𝑢 ∈
𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) |
38 | 37, 18, 13 | wral 3065 |
. . . . . . . 8
wff
∀𝑧 ∈
𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) |
39 | 38, 2, 13 | wral 3065 |
. . . . . . 7
wff
∀𝑦 ∈
𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) |
40 | 39, 4, 13 | wral 3065 |
. . . . . 6
wff
∀𝑥 ∈
𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) |
41 | 28, 3, 7 | co 7268 |
. . . . . . . . . . . . 13
class (𝑎𝑖𝑦) |
42 | 5, 41 | wcel 2109 |
. . . . . . . . . . . 12
wff 𝑥 ∈ (𝑎𝑖𝑦) |
43 | | vt |
. . . . . . . . . . . . 13
setvar 𝑡 |
44 | 43 | cv 1540 |
. . . . . . . . . . . 12
class 𝑡 |
45 | 42, 2, 44 | wral 3065 |
. . . . . . . . . . 11
wff
∀𝑦 ∈
𝑡 𝑥 ∈ (𝑎𝑖𝑦) |
46 | | vs |
. . . . . . . . . . . 12
setvar 𝑠 |
47 | 46 | cv 1540 |
. . . . . . . . . . 11
class 𝑠 |
48 | 45, 4, 47 | wral 3065 |
. . . . . . . . . 10
wff
∀𝑥 ∈
𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) |
49 | 48, 27, 13 | wrex 3066 |
. . . . . . . . 9
wff
∃𝑎 ∈
𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) |
50 | | vb |
. . . . . . . . . . . . . 14
setvar 𝑏 |
51 | 50 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑏 |
52 | 5, 3, 7 | co 7268 |
. . . . . . . . . . . . 13
class (𝑥𝑖𝑦) |
53 | 51, 52 | wcel 2109 |
. . . . . . . . . . . 12
wff 𝑏 ∈ (𝑥𝑖𝑦) |
54 | 53, 2, 44 | wral 3065 |
. . . . . . . . . . 11
wff
∀𝑦 ∈
𝑡 𝑏 ∈ (𝑥𝑖𝑦) |
55 | 54, 4, 47 | wral 3065 |
. . . . . . . . . 10
wff
∀𝑥 ∈
𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦) |
56 | 55, 50, 13 | wrex 3066 |
. . . . . . . . 9
wff
∃𝑏 ∈
𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦) |
57 | 49, 56 | wi 4 |
. . . . . . . 8
wff
(∃𝑎 ∈
𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)) |
58 | 13 | cpw 4538 |
. . . . . . . 8
class 𝒫
𝑝 |
59 | 57, 43, 58 | wral 3065 |
. . . . . . 7
wff
∀𝑡 ∈
𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)) |
60 | 59, 46, 58 | wral 3065 |
. . . . . 6
wff
∀𝑠 ∈
𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)) |
61 | 15, 40, 60 | w3a 1085 |
. . . . 5
wff
(∀𝑥 ∈
𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦))) |
62 | | vf |
. . . . . . 7
setvar 𝑓 |
63 | 62 | cv 1540 |
. . . . . 6
class 𝑓 |
64 | | citv 26775 |
. . . . . 6
class
Itv |
65 | 63, 64 | cfv 6430 |
. . . . 5
class
(Itv‘𝑓) |
66 | 61, 6, 65 | wsbc 3719 |
. . . 4
wff
[(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦))) |
67 | | cbs 16893 |
. . . . 5
class
Base |
68 | 63, 67 | cfv 6430 |
. . . 4
class
(Base‘𝑓) |
69 | 66, 12, 68 | wsbc 3719 |
. . 3
wff
[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦))) |
70 | 69, 62 | cab 2716 |
. 2
class {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))} |
71 | 1, 70 | wceq 1541 |
1
wff
TarskiGB = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎 ∈ 𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝∀𝑡 ∈ 𝒫 𝑝(∃𝑎 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏 ∈ 𝑝 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝑖𝑦)))} |