Detailed syntax breakdown of Definition df-hmeo
Step | Hyp | Ref
| Expression |
1 | | chmeo 22650 |
. 2
class
Homeo |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | vk |
. . 3
setvar 𝑘 |
4 | | ctop 21790 |
. . 3
class
Top |
5 | | vf |
. . . . . . 7
setvar 𝑓 |
6 | 5 | cv 1542 |
. . . . . 6
class 𝑓 |
7 | 6 | ccnv 5550 |
. . . . 5
class ◡𝑓 |
8 | 3 | cv 1542 |
. . . . . 6
class 𝑘 |
9 | 2 | cv 1542 |
. . . . . 6
class 𝑗 |
10 | | ccn 22121 |
. . . . . 6
class
Cn |
11 | 8, 9, 10 | co 7213 |
. . . . 5
class (𝑘 Cn 𝑗) |
12 | 7, 11 | wcel 2110 |
. . . 4
wff ◡𝑓 ∈ (𝑘 Cn 𝑗) |
13 | 9, 8, 10 | co 7213 |
. . . 4
class (𝑗 Cn 𝑘) |
14 | 12, 5, 13 | crab 3065 |
. . 3
class {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)} |
15 | 2, 3, 4, 4, 14 | cmpo 7215 |
. 2
class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)}) |
16 | 1, 15 | wceq 1543 |
1
wff Homeo =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)}) |