Step | Hyp | Ref
| Expression |
1 | | cghomOLD 36392 |
. 2
class
GrpOpHom |
2 | | vg |
. . 3
setvar π |
3 | | vh |
. . 3
setvar β |
4 | | cgr 29480 |
. . 3
class
GrpOp |
5 | 2 | cv 1541 |
. . . . . . 7
class π |
6 | 5 | crn 5638 |
. . . . . 6
class ran π |
7 | 3 | cv 1541 |
. . . . . . 7
class β |
8 | 7 | crn 5638 |
. . . . . 6
class ran β |
9 | | vf |
. . . . . . 7
setvar π |
10 | 9 | cv 1541 |
. . . . . 6
class π |
11 | 6, 8, 10 | wf 6496 |
. . . . 5
wff π:ran πβΆran β |
12 | | vx |
. . . . . . . . . . 11
setvar π₯ |
13 | 12 | cv 1541 |
. . . . . . . . . 10
class π₯ |
14 | 13, 10 | cfv 6500 |
. . . . . . . . 9
class (πβπ₯) |
15 | | vy |
. . . . . . . . . . 11
setvar π¦ |
16 | 15 | cv 1541 |
. . . . . . . . . 10
class π¦ |
17 | 16, 10 | cfv 6500 |
. . . . . . . . 9
class (πβπ¦) |
18 | 14, 17, 7 | co 7361 |
. . . . . . . 8
class ((πβπ₯)β(πβπ¦)) |
19 | 13, 16, 5 | co 7361 |
. . . . . . . . 9
class (π₯ππ¦) |
20 | 19, 10 | cfv 6500 |
. . . . . . . 8
class (πβ(π₯ππ¦)) |
21 | 18, 20 | wceq 1542 |
. . . . . . 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 397 |
. . . 4
wff (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦))) |
25 | 24, 9 | cab 2710 |
. . 3
class {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))} |
26 | 2, 3, 4, 4, 25 | cmpo 7363 |
. 2
class (π β GrpOp, β β GrpOp β¦ {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))}) |
27 | 1, 26 | wceq 1542 |
1
wff GrpOpHom =
(π β GrpOp, β β GrpOp β¦ {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))}) |