Detailed syntax breakdown of Definition df-0g
Step | Hyp | Ref
| Expression |
1 | | c0g 17148 |
. 2
class
0g |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3431 |
. . 3
class
V |
4 | | ve |
. . . . . . 7
setvar 𝑒 |
5 | 4 | cv 1541 |
. . . . . 6
class 𝑒 |
6 | 2 | cv 1541 |
. . . . . . 7
class 𝑔 |
7 | | cbs 16910 |
. . . . . . 7
class
Base |
8 | 6, 7 | cfv 6432 |
. . . . . 6
class
(Base‘𝑔) |
9 | 5, 8 | wcel 2110 |
. . . . 5
wff 𝑒 ∈ (Base‘𝑔) |
10 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
11 | 10 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
12 | | cplusg 16960 |
. . . . . . . . . 10
class
+g |
13 | 6, 12 | cfv 6432 |
. . . . . . . . 9
class
(+g‘𝑔) |
14 | 5, 11, 13 | co 7271 |
. . . . . . . 8
class (𝑒(+g‘𝑔)𝑥) |
15 | 14, 11 | wceq 1542 |
. . . . . . 7
wff (𝑒(+g‘𝑔)𝑥) = 𝑥 |
16 | 11, 5, 13 | co 7271 |
. . . . . . . 8
class (𝑥(+g‘𝑔)𝑒) |
17 | 16, 11 | wceq 1542 |
. . . . . . 7
wff (𝑥(+g‘𝑔)𝑒) = 𝑥 |
18 | 15, 17 | wa 396 |
. . . . . 6
wff ((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥) |
19 | 18, 10, 8 | wral 3066 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥) |
20 | 9, 19 | wa 396 |
. . . 4
wff (𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)) |
21 | 20, 4 | cio 6388 |
. . 3
class
(℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))) |
22 | 2, 3, 21 | cmpt 5162 |
. 2
class (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) |
23 | 1, 22 | wceq 1542 |
1
wff
0g = (𝑔
∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) |