Description: The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cnfldtopn.1 | |- J = ( TopOpen ` CCfld ) |
|
| Assertion | cnfldhaus | |- J e. Haus |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnfldtopn.1 | |- J = ( TopOpen ` CCfld ) |
|
| 2 | cnxmet | |- ( abs o. - ) e. ( *Met ` CC ) |
|
| 3 | 1 | cnfldtopn | |- J = ( MetOpen ` ( abs o. - ) ) |
| 4 | 3 | methaus | |- ( ( abs o. - ) e. ( *Met ` CC ) -> J e. Haus ) |
| 5 | 2 4 | ax-mp | |- J e. Haus |