Detailed syntax breakdown of Definition df-trkge
Step | Hyp | Ref
| Expression |
1 | | cstrkge 26526 |
. 2
class
TarskiGE |
2 | | vu |
. . . . . . . . . . . . . 14
setvar 𝑢 |
3 | 2 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑢 |
4 | | vx |
. . . . . . . . . . . . . . 15
setvar 𝑥 |
5 | 4 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑥 |
6 | | vv |
. . . . . . . . . . . . . . 15
setvar 𝑣 |
7 | 6 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑣 |
8 | | vi |
. . . . . . . . . . . . . . 15
setvar 𝑖 |
9 | 8 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑖 |
10 | 5, 7, 9 | co 7213 |
. . . . . . . . . . . . 13
class (𝑥𝑖𝑣) |
11 | 3, 10 | wcel 2110 |
. . . . . . . . . . . 12
wff 𝑢 ∈ (𝑥𝑖𝑣) |
12 | | vy |
. . . . . . . . . . . . . . 15
setvar 𝑦 |
13 | 12 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑦 |
14 | | vz |
. . . . . . . . . . . . . . 15
setvar 𝑧 |
15 | 14 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑧 |
16 | 13, 15, 9 | co 7213 |
. . . . . . . . . . . . 13
class (𝑦𝑖𝑧) |
17 | 3, 16 | wcel 2110 |
. . . . . . . . . . . 12
wff 𝑢 ∈ (𝑦𝑖𝑧) |
18 | 5, 3 | wne 2940 |
. . . . . . . . . . . 12
wff 𝑥 ≠ 𝑢 |
19 | 11, 17, 18 | w3a 1089 |
. . . . . . . . . . 11
wff (𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) |
20 | | va |
. . . . . . . . . . . . . . . . 17
setvar 𝑎 |
21 | 20 | cv 1542 |
. . . . . . . . . . . . . . . 16
class 𝑎 |
22 | 5, 21, 9 | co 7213 |
. . . . . . . . . . . . . . 15
class (𝑥𝑖𝑎) |
23 | 13, 22 | wcel 2110 |
. . . . . . . . . . . . . 14
wff 𝑦 ∈ (𝑥𝑖𝑎) |
24 | | vb |
. . . . . . . . . . . . . . . . 17
setvar 𝑏 |
25 | 24 | cv 1542 |
. . . . . . . . . . . . . . . 16
class 𝑏 |
26 | 5, 25, 9 | co 7213 |
. . . . . . . . . . . . . . 15
class (𝑥𝑖𝑏) |
27 | 15, 26 | wcel 2110 |
. . . . . . . . . . . . . 14
wff 𝑧 ∈ (𝑥𝑖𝑏) |
28 | 21, 25, 9 | co 7213 |
. . . . . . . . . . . . . . 15
class (𝑎𝑖𝑏) |
29 | 7, 28 | wcel 2110 |
. . . . . . . . . . . . . 14
wff 𝑣 ∈ (𝑎𝑖𝑏) |
30 | 23, 27, 29 | w3a 1089 |
. . . . . . . . . . . . 13
wff (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)) |
31 | | vp |
. . . . . . . . . . . . . 14
setvar 𝑝 |
32 | 31 | cv 1542 |
. . . . . . . . . . . . 13
class 𝑝 |
33 | 30, 24, 32 | wrex 3062 |
. . . . . . . . . . . 12
wff
∃𝑏 ∈
𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)) |
34 | 33, 20, 32 | wrex 3062 |
. . . . . . . . . . 11
wff
∃𝑎 ∈
𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)) |
35 | 19, 34 | wi 4 |
. . . . . . . . . 10
wff ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
36 | 35, 6, 32 | wral 3061 |
. . . . . . . . 9
wff
∀𝑣 ∈
𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
37 | 36, 2, 32 | wral 3061 |
. . . . . . . 8
wff
∀𝑢 ∈
𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
38 | 37, 14, 32 | wral 3061 |
. . . . . . 7
wff
∀𝑧 ∈
𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
39 | 38, 12, 32 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
40 | 39, 4, 32 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈
𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
41 | | vf |
. . . . . . 7
setvar 𝑓 |
42 | 41 | cv 1542 |
. . . . . 6
class 𝑓 |
43 | | citv 26527 |
. . . . . 6
class
Itv |
44 | 42, 43 | cfv 6380 |
. . . . 5
class
(Itv‘𝑓) |
45 | 40, 8, 44 | wsbc 3694 |
. . . 4
wff
[(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
46 | | cbs 16760 |
. . . . 5
class
Base |
47 | 42, 46 | cfv 6380 |
. . . 4
class
(Base‘𝑓) |
48 | 45, 31, 47 | wsbc 3694 |
. . 3
wff
[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))) |
49 | 48, 41 | cab 2714 |
. 2
class {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))} |
50 | 1, 49 | wceq 1543 |
1
wff
TarskiGE = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ∀𝑢 ∈ 𝑝 ∀𝑣 ∈ 𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑝 ∃𝑏 ∈ 𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))} |