Detailed syntax breakdown of Definition df-eqg
Step | Hyp | Ref
| Expression |
1 | | cqg 18760 |
. 2
class
~QG |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vi |
. . 3
setvar 𝑖 |
4 | | cvv 3433 |
. . 3
class
V |
5 | | vx |
. . . . . . . 8
setvar 𝑥 |
6 | 5 | cv 1538 |
. . . . . . 7
class 𝑥 |
7 | | vy |
. . . . . . . 8
setvar 𝑦 |
8 | 7 | cv 1538 |
. . . . . . 7
class 𝑦 |
9 | 6, 8 | cpr 4564 |
. . . . . 6
class {𝑥, 𝑦} |
10 | 2 | cv 1538 |
. . . . . . 7
class 𝑟 |
11 | | cbs 16921 |
. . . . . . 7
class
Base |
12 | 10, 11 | cfv 6437 |
. . . . . 6
class
(Base‘𝑟) |
13 | 9, 12 | wss 3888 |
. . . . 5
wff {𝑥, 𝑦} ⊆ (Base‘𝑟) |
14 | | cminusg 18587 |
. . . . . . . . 9
class
invg |
15 | 10, 14 | cfv 6437 |
. . . . . . . 8
class
(invg‘𝑟) |
16 | 6, 15 | cfv 6437 |
. . . . . . 7
class
((invg‘𝑟)‘𝑥) |
17 | | cplusg 16971 |
. . . . . . . 8
class
+g |
18 | 10, 17 | cfv 6437 |
. . . . . . 7
class
(+g‘𝑟) |
19 | 16, 8, 18 | co 7284 |
. . . . . 6
class
(((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) |
20 | 3 | cv 1538 |
. . . . . 6
class 𝑖 |
21 | 19, 20 | wcel 2107 |
. . . . 5
wff
(((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖 |
22 | 13, 21 | wa 396 |
. . . 4
wff ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖) |
23 | 22, 5, 7 | copab 5137 |
. . 3
class
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)} |
24 | 2, 3, 4, 4, 23 | cmpo 7286 |
. 2
class (𝑟 ∈ V, 𝑖 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)}) |
25 | 1, 24 | wceq 1539 |
1
wff
~QG = (𝑟
∈ V, 𝑖 ∈ V
↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)}) |