Theorem oninhaus

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

	Ref	Expression
Assertion	oninhaus	$$⊢\mathrm{On}\cap \mathrm{Haus}=\left\{1_{𝑜},2_{𝑜}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		haust1	$$⊢x\in \mathrm{Haus}\to x\in \mathrm{Fre}$$
2	1	ssriv	$$⊢\mathrm{Haus}\subseteq \mathrm{Fre}$$
3		sslin	$$⊢\mathrm{Haus}\subseteq \mathrm{Fre}\to \mathrm{On}\cap \mathrm{Haus}\subseteq \mathrm{On}\cap \mathrm{Fre}$$
4	2 3	ax-mp	$$⊢\mathrm{On}\cap \mathrm{Haus}\subseteq \mathrm{On}\cap \mathrm{Fre}$$
5		onint1	$$⊢\mathrm{On}\cap \mathrm{Fre}=\left\{1_{𝑜},2_{𝑜}\right\}$$
6	4 5	sseqtri	$$⊢\mathrm{On}\cap \mathrm{Haus}\subseteq \left\{1_{𝑜},2_{𝑜}\right\}$$
7		ssoninhaus	$$⊢\left\{1_{𝑜},2_{𝑜}\right\}\subseteq \mathrm{On}\cap \mathrm{Haus}$$
8	6 7	eqssi	$$⊢\mathrm{On}\cap \mathrm{Haus}=\left\{1_{𝑜},2_{𝑜}\right\}$$