Description: A T_1 normal space is Hausdorff. A Hausdorff or T_1 normal space is also known as a T_4 space. (Contributed by Mario Carneiro, 24-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nrmhaus | |- ( J e. Nrm -> ( J e. Haus <-> J e. Fre ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | haust1 | |- ( J e. Haus -> J e. Fre ) |
|
| 2 | nrmreg | |- ( ( J e. Nrm /\ J e. Fre ) -> J e. Reg ) |
|
| 3 | 2 | ex | |- ( J e. Nrm -> ( J e. Fre -> J e. Reg ) ) |
| 4 | t1t0 | |- ( J e. Fre -> J e. Kol2 ) |
|
| 5 | reghaus | |- ( J e. Reg -> ( J e. Haus <-> J e. Kol2 ) ) |
|
| 6 | 4 5 | syl5ibrcom | |- ( J e. Fre -> ( J e. Reg -> J e. Haus ) ) |
| 7 | 3 6 | sylcom | |- ( J e. Nrm -> ( J e. Fre -> J e. Haus ) ) |
| 8 | 1 7 | impbid2 | |- ( J e. Nrm -> ( J e. Haus <-> J e. Fre ) ) |