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 } ⊆ ( On ∩ Haus )

Proof

Step	Hyp	Ref	Expression
1		1on	⊢ 1o ∈ On
2		2on	⊢ 2o ∈ On
3		prssi	⊢ ( ( 1o ∈ On ∧ 2o ∈ On ) → { 1o , 2o } ⊆ On )
4	1 2 3	mp2an	⊢ { 1o , 2o } ⊆ On
5		df1o2	⊢ 1o = { ∅ }
6		pw0	⊢ 𝒫 ∅ = { ∅ }
7	5 6	eqtr4i	⊢ 1o = 𝒫 ∅
8		0ex	⊢ ∅ ∈ V
9		dishaus	⊢ ( ∅ ∈ V → 𝒫 ∅ ∈ Haus )
10	8 9	ax-mp	⊢ 𝒫 ∅ ∈ Haus
11	7 10	eqeltri	⊢ 1o ∈ Haus
12		df2o2	⊢ 2o = { ∅ , { ∅ } }
13		pwpw0	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }
14	12 13	eqtr4i	⊢ 2o = 𝒫 { ∅ }
15		p0ex	⊢ { ∅ } ∈ V
16		dishaus	⊢ ( { ∅ } ∈ V → 𝒫 { ∅ } ∈ Haus )
17	15 16	ax-mp	⊢ 𝒫 { ∅ } ∈ Haus
18	14 17	eqeltri	⊢ 2o ∈ Haus
19		prssi	⊢ ( ( 1o ∈ Haus ∧ 2o ∈ Haus ) → { 1o , 2o } ⊆ Haus )
20	11 18 19	mp2an	⊢ { 1o , 2o } ⊆ Haus
21	4 20	ssini	⊢ { 1o , 2o } ⊆ ( On ∩ Haus )