Description: The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hmphtop1 | |- ( J ~= K -> J e. Top ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hmphtop | |- ( J ~= K -> ( J e. Top /\ K e. Top ) ) |
|
| 2 | 1 | simpld | |- ( J ~= K -> J e. Top ) |