Detailed syntax breakdown of Definition df-grpo
Step | Hyp | Ref
| Expression |
1 | | cgr 28570 |
. 2
class
GrpOp |
2 | | vt |
. . . . . . . 8
setvar 𝑡 |
3 | 2 | cv 1542 |
. . . . . . 7
class 𝑡 |
4 | 3, 3 | cxp 5549 |
. . . . . 6
class (𝑡 × 𝑡) |
5 | | vg |
. . . . . . 7
setvar 𝑔 |
6 | 5 | cv 1542 |
. . . . . 6
class 𝑔 |
7 | 4, 3, 6 | wf 6376 |
. . . . 5
wff 𝑔:(𝑡 × 𝑡)⟶𝑡 |
8 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
9 | 8 | cv 1542 |
. . . . . . . . . . 11
class 𝑥 |
10 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
11 | 10 | cv 1542 |
. . . . . . . . . . 11
class 𝑦 |
12 | 9, 11, 6 | co 7213 |
. . . . . . . . . 10
class (𝑥𝑔𝑦) |
13 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
14 | 13 | cv 1542 |
. . . . . . . . . 10
class 𝑧 |
15 | 12, 14, 6 | co 7213 |
. . . . . . . . 9
class ((𝑥𝑔𝑦)𝑔𝑧) |
16 | 11, 14, 6 | co 7213 |
. . . . . . . . . 10
class (𝑦𝑔𝑧) |
17 | 9, 16, 6 | co 7213 |
. . . . . . . . 9
class (𝑥𝑔(𝑦𝑔𝑧)) |
18 | 15, 17 | wceq 1543 |
. . . . . . . 8
wff ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
19 | 18, 13, 3 | wral 3061 |
. . . . . . 7
wff
∀𝑧 ∈
𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
20 | 19, 10, 3 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
21 | 20, 8, 3 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈
𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) |
22 | | vu |
. . . . . . . . . . 11
setvar 𝑢 |
23 | 22 | cv 1542 |
. . . . . . . . . 10
class 𝑢 |
24 | 23, 9, 6 | co 7213 |
. . . . . . . . 9
class (𝑢𝑔𝑥) |
25 | 24, 9 | wceq 1543 |
. . . . . . . 8
wff (𝑢𝑔𝑥) = 𝑥 |
26 | 11, 9, 6 | co 7213 |
. . . . . . . . . 10
class (𝑦𝑔𝑥) |
27 | 26, 23 | wceq 1543 |
. . . . . . . . 9
wff (𝑦𝑔𝑥) = 𝑢 |
28 | 27, 10, 3 | wrex 3062 |
. . . . . . . 8
wff
∃𝑦 ∈
𝑡 (𝑦𝑔𝑥) = 𝑢 |
29 | 25, 28 | wa 399 |
. . . . . . 7
wff ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) |
30 | 29, 8, 3 | wral 3061 |
. . . . . 6
wff
∀𝑥 ∈
𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) |
31 | 30, 22, 3 | wrex 3062 |
. . . . 5
wff
∃𝑢 ∈
𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢) |
32 | 7, 21, 31 | w3a 1089 |
. . . 4
wff (𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)) |
33 | 32, 2 | wex 1787 |
. . 3
wff
∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢)) |
34 | 33, 5 | cab 2714 |
. 2
class {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} |
35 | 1, 34 | wceq 1543 |
1
wff GrpOp =
{𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))} |