Theorem ssoninhaus

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

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

Proof

Step	Hyp	Ref	Expression
1		1on	|- 1o e. On
2		2on	|- 2o e. On
3		prssi	|- ( ( 1o e. On /\ 2o e. On ) -> { 1o , 2o } C_ On )
4	1 2 3	mp2an	|- { 1o , 2o } C_ On
5		df1o2	|- 1o = { (/) }
6		pw0	|- ~P (/) = { (/) }
7	5 6	eqtr4i	|- 1o = ~P (/)
8		0ex	|- (/) e. _V
9		dishaus	|- ( (/) e. _V -> ~P (/) e. Haus )
10	8 9	ax-mp	|- ~P (/) e. Haus
11	7 10	eqeltri	|- 1o e. Haus
12		df2o2	|- 2o = { (/) , { (/) } }
13		pwpw0	|- ~P { (/) } = { (/) , { (/) } }
14	12 13	eqtr4i	|- 2o = ~P { (/) }
15		p0ex	|- { (/) } e. _V
16		dishaus	|- ( { (/) } e. _V -> ~P { (/) } e. Haus )
17	15 16	ax-mp	|- ~P { (/) } e. Haus
18	14 17	eqeltri	|- 2o e. Haus
19		prssi	|- ( ( 1o e. Haus /\ 2o e. Haus ) -> { 1o , 2o } C_ Haus )
20	11 18 19	mp2an	|- { 1o , 2o } C_ Haus
21	4 20	ssini	|- { 1o , 2o } C_ ( On i^i Haus )