![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-hmph | Structured version Visualization version GIF version |
Description: Definition of the relation 𝑥 is homeomorphic to 𝑦. (Contributed by FL, 14-Feb-2007.) |
Ref | Expression |
---|---|
df-hmph | ⊢ ≃ = (◡Homeo “ (V ∖ 1𝑜)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chmph 21886 | . 2 class ≃ | |
2 | chmeo 21885 | . . . 4 class Homeo | |
3 | 2 | ccnv 5311 | . . 3 class ◡Homeo |
4 | cvv 3385 | . . . 4 class V | |
5 | c1o 7792 | . . . 4 class 1𝑜 | |
6 | 4, 5 | cdif 3766 | . . 3 class (V ∖ 1𝑜) |
7 | 3, 6 | cima 5315 | . 2 class (◡Homeo “ (V ∖ 1𝑜)) |
8 | 1, 7 | wceq 1653 | 1 wff ≃ = (◡Homeo “ (V ∖ 1𝑜)) |
Colors of variables: wff setvar class |
This definition is referenced by: hmph 21908 hmphtop 21910 hmpher 21916 |
Copyright terms: Public domain | W3C validator |