Metamath Proof Explorer


Theorem oninhaus

Description: The ordinal Hausdorff spaces are 1o and 2o . (Contributed by Chen-Pang He, 10-Nov-2015)

Ref Expression
Assertion oninhaus OnHaus=1𝑜2𝑜

Proof

Step Hyp Ref Expression
1 haust1 xHausxFre
2 1 ssriv HausFre
3 sslin HausFreOnHausOnFre
4 2 3 ax-mp OnHausOnFre
5 onint1 OnFre=1𝑜2𝑜
6 4 5 sseqtri OnHaus1𝑜2𝑜
7 ssoninhaus 1𝑜2𝑜OnHaus
8 6 7 eqssi OnHaus=1𝑜2𝑜