Step | Hyp | Ref
| Expression |
1 | | ctng 23937 |
. 2
class
toNrmGrp |
2 | | vg |
. . 3
setvar ๐ |
3 | | vf |
. . 3
setvar ๐ |
4 | | cvv 3446 |
. . 3
class
V |
5 | 2 | cv 1541 |
. . . . 5
class ๐ |
6 | | cnx 17066 |
. . . . . . 7
class
ndx |
7 | | cds 17143 |
. . . . . . 7
class
dist |
8 | 6, 7 | cfv 6497 |
. . . . . 6
class
(distโndx) |
9 | 3 | cv 1541 |
. . . . . . 7
class ๐ |
10 | | csg 18751 |
. . . . . . . 8
class
-g |
11 | 5, 10 | cfv 6497 |
. . . . . . 7
class
(-gโ๐) |
12 | 9, 11 | ccom 5638 |
. . . . . 6
class (๐ โ
(-gโ๐)) |
13 | 8, 12 | cop 4593 |
. . . . 5
class
โจ(distโndx), (๐ โ (-gโ๐))โฉ |
14 | | csts 17036 |
. . . . 5
class
sSet |
15 | 5, 13, 14 | co 7358 |
. . . 4
class (๐ sSet โจ(distโndx),
(๐ โ
(-gโ๐))โฉ) |
16 | | cts 17140 |
. . . . . 6
class
TopSet |
17 | 6, 16 | cfv 6497 |
. . . . 5
class
(TopSetโndx) |
18 | | cmopn 20789 |
. . . . . 6
class
MetOpen |
19 | 12, 18 | cfv 6497 |
. . . . 5
class
(MetOpenโ(๐
โ (-gโ๐))) |
20 | 17, 19 | cop 4593 |
. . . 4
class
โจ(TopSetโndx), (MetOpenโ(๐ โ (-gโ๐)))โฉ |
21 | 15, 20, 14 | co 7358 |
. . 3
class ((๐ sSet โจ(distโndx),
(๐ โ
(-gโ๐))โฉ) sSet โจ(TopSetโndx),
(MetOpenโ(๐ โ
(-gโ๐)))โฉ) |
22 | 2, 3, 4, 4, 21 | cmpo 7360 |
. 2
class (๐ โ V, ๐ โ V โฆ ((๐ sSet โจ(distโndx), (๐ โ
(-gโ๐))โฉ) sSet โจ(TopSetโndx),
(MetOpenโ(๐ โ
(-gโ๐)))โฉ)) |
23 | 1, 22 | wceq 1542 |
1
wff toNrmGrp =
(๐ โ V, ๐ โ V โฆ ((๐ sSet โจ(distโndx),
(๐ โ
(-gโ๐))โฉ) sSet โจ(TopSetโndx),
(MetOpenโ(๐ โ
(-gโ๐)))โฉ)) |