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 ) = { 1o , 2o }

Proof

Step	Hyp	Ref	Expression
1		haust1	⊢ ( 𝑥 ∈ Haus → 𝑥 ∈ 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 ) = { 1o , 2o }
6	4 5	sseqtri	⊢ ( On ∩ Haus ) ⊆ { 1o , 2o }
7		ssoninhaus	⊢ { 1o , 2o } ⊆ ( On ∩ Haus )
8	6 7	eqssi	⊢ ( On ∩ Haus ) = { 1o , 2o }