Step | Hyp | Ref
| Expression |
1 | | csx 32454 |
. 2
class
Γs |
2 | | vs |
. . 3
setvar π |
3 | | vt |
. . 3
setvar π‘ |
4 | | cvv 3441 |
. . 3
class
V |
5 | | vx |
. . . . . 6
setvar π₯ |
6 | | vy |
. . . . . 6
setvar π¦ |
7 | 2 | cv 1539 |
. . . . . 6
class π |
8 | 3 | cv 1539 |
. . . . . 6
class π‘ |
9 | 5 | cv 1539 |
. . . . . . 7
class π₯ |
10 | 6 | cv 1539 |
. . . . . . 7
class π¦ |
11 | 9, 10 | cxp 5618 |
. . . . . 6
class (π₯ Γ π¦) |
12 | 5, 6, 7, 8, 11 | cmpo 7339 |
. . . . 5
class (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)) |
13 | 12 | crn 5621 |
. . . 4
class ran
(π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)) |
14 | | csigagen 32404 |
. . . 4
class
sigaGen |
15 | 13, 14 | cfv 6479 |
. . 3
class
(sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦))) |
16 | 2, 3, 4, 4, 15 | cmpo 7339 |
. 2
class (π β V, π‘ β V β¦ (sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)))) |
17 | 1, 16 | wceq 1540 |
1
wff
Γs = (π
β V, π‘ β V
β¦ (sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)))) |