Detailed syntax breakdown of Definition df-tng
Step | Hyp | Ref
| Expression |
1 | | ctng 23503 |
. 2
class
toNrmGrp |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3421 |
. . 3
class
V |
5 | 2 | cv 1542 |
. . . . 5
class 𝑔 |
6 | | cnx 16772 |
. . . . . . 7
class
ndx |
7 | | cds 16839 |
. . . . . . 7
class
dist |
8 | 6, 7 | cfv 6398 |
. . . . . 6
class
(dist‘ndx) |
9 | 3 | cv 1542 |
. . . . . . 7
class 𝑓 |
10 | | csg 18395 |
. . . . . . . 8
class
-g |
11 | 5, 10 | cfv 6398 |
. . . . . . 7
class
(-g‘𝑔) |
12 | 9, 11 | ccom 5570 |
. . . . . 6
class (𝑓 ∘
(-g‘𝑔)) |
13 | 8, 12 | cop 4562 |
. . . . 5
class
〈(dist‘ndx), (𝑓 ∘ (-g‘𝑔))〉 |
14 | | csts 16744 |
. . . . 5
class
sSet |
15 | 5, 13, 14 | co 7232 |
. . . 4
class (𝑔 sSet 〈(dist‘ndx),
(𝑓 ∘
(-g‘𝑔))〉) |
16 | | cts 16836 |
. . . . . 6
class
TopSet |
17 | 6, 16 | cfv 6398 |
. . . . 5
class
(TopSet‘ndx) |
18 | | cmopn 20381 |
. . . . . 6
class
MetOpen |
19 | 12, 18 | cfv 6398 |
. . . . 5
class
(MetOpen‘(𝑓
∘ (-g‘𝑔))) |
20 | 17, 19 | cop 4562 |
. . . 4
class
〈(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))〉 |
21 | 15, 20, 14 | co 7232 |
. . 3
class ((𝑔 sSet 〈(dist‘ndx),
(𝑓 ∘
(-g‘𝑔))〉) sSet 〈(TopSet‘ndx),
(MetOpen‘(𝑓 ∘
(-g‘𝑔)))〉) |
22 | 2, 3, 4, 4, 21 | cmpo 7234 |
. 2
class (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet 〈(dist‘ndx), (𝑓 ∘
(-g‘𝑔))〉) sSet 〈(TopSet‘ndx),
(MetOpen‘(𝑓 ∘
(-g‘𝑔)))〉)) |
23 | 1, 22 | wceq 1543 |
1
wff toNrmGrp =
(𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet 〈(dist‘ndx),
(𝑓 ∘
(-g‘𝑔))〉) sSet 〈(TopSet‘ndx),
(MetOpen‘(𝑓 ∘
(-g‘𝑔)))〉)) |