Theorem oninhaus

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

	Ref	Expression
Assertion	oninhaus	|- ( On i^i Haus ) = { 1o , 2o }

Proof

Step	Hyp	Ref	Expression
1		haust1	|- ( x e. Haus -> x e. Fre )
2	1	ssriv	|- Haus C_ Fre
3		sslin	|- ( Haus C_ Fre -> ( On i^i Haus ) C_ ( On i^i Fre ) )
4	2 3	ax-mp	|- ( On i^i Haus ) C_ ( On i^i Fre )
5		onint1	|- ( On i^i Fre ) = { 1o , 2o }
6	4 5	sseqtri	|- ( On i^i Haus ) C_ { 1o , 2o }
7		ssoninhaus	|- { 1o , 2o } C_ ( On i^i Haus )
8	6 7	eqssi	|- ( On i^i Haus ) = { 1o , 2o }