Detailed syntax breakdown of Definition df-ghomOLD
Step | Hyp | Ref
| Expression |
1 | | cghomOLD 35778 |
. 2
class
GrpOpHom |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | vh |
. . 3
setvar ℎ |
4 | | cgr 28570 |
. . 3
class
GrpOp |
5 | 2 | cv 1542 |
. . . . . . 7
class 𝑔 |
6 | 5 | crn 5552 |
. . . . . 6
class ran 𝑔 |
7 | 3 | cv 1542 |
. . . . . . 7
class ℎ |
8 | 7 | crn 5552 |
. . . . . 6
class ran ℎ |
9 | | vf |
. . . . . . 7
setvar 𝑓 |
10 | 9 | cv 1542 |
. . . . . 6
class 𝑓 |
11 | 6, 8, 10 | wf 6376 |
. . . . 5
wff 𝑓:ran 𝑔⟶ran ℎ |
12 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
13 | 12 | cv 1542 |
. . . . . . . . . 10
class 𝑥 |
14 | 13, 10 | cfv 6380 |
. . . . . . . . 9
class (𝑓‘𝑥) |
15 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
16 | 15 | cv 1542 |
. . . . . . . . . 10
class 𝑦 |
17 | 16, 10 | cfv 6380 |
. . . . . . . . 9
class (𝑓‘𝑦) |
18 | 14, 17, 7 | co 7213 |
. . . . . . . 8
class ((𝑓‘𝑥)ℎ(𝑓‘𝑦)) |
19 | 13, 16, 5 | co 7213 |
. . . . . . . . 9
class (𝑥𝑔𝑦) |
20 | 19, 10 | cfv 6380 |
. . . . . . . 8
class (𝑓‘(𝑥𝑔𝑦)) |
21 | 18, 20 | wceq 1543 |
. . . . . . 7
wff ((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)) |
22 | 21, 15, 6 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈ ran
𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)) |
23 | 22, 12, 6 | wral 3061 |
. . . . 5
wff
∀𝑥 ∈ ran
𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)) |
24 | 11, 23 | wa 399 |
. . . 4
wff (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦))) |
25 | 24, 9 | cab 2714 |
. . 3
class {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))} |
26 | 2, 3, 4, 4, 25 | cmpo 7215 |
. 2
class (𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))}) |
27 | 1, 26 | wceq 1543 |
1
wff GrpOpHom =
(𝑔 ∈ GrpOp, ℎ ∈ GrpOp ↦ {𝑓 ∣ (𝑓:ran 𝑔⟶ran ℎ ∧ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑓‘𝑥)ℎ(𝑓‘𝑦)) = (𝑓‘(𝑥𝑔𝑦)))}) |