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 On Haus = 1 𝑜 2 𝑜

Proof

Step Hyp Ref Expression
1 haust1 x Haus x Fre
2 1 ssriv Haus Fre
3 sslin Haus Fre On Haus On Fre
4 2 3 ax-mp On Haus On Fre
5 onint1 On Fre = 1 𝑜 2 𝑜
6 4 5 sseqtri On Haus 1 𝑜 2 𝑜
7 ssoninhaus 1 𝑜 2 𝑜 On Haus
8 6 7 eqssi On Haus = 1 𝑜 2 𝑜