Theorem ssoninhaus

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

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

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
3		prssi	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge 2_{𝑜}\in \mathrm{On}\right)\to \left\{1_{𝑜},2_{𝑜}\right\}\subseteq \mathrm{On}$$
4	1 2 3	mp2an	$$⊢\left\{1_{𝑜},2_{𝑜}\right\}\subseteq \mathrm{On}$$
5		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
6		pw0	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$
7	5 6	eqtr4i	$$⊢1_{𝑜}=𝒫\varnothing$$
8		0ex	$$⊢\varnothing \in \mathrm{V}$$
9		dishaus	$$⊢\varnothing \in \mathrm{V}\to 𝒫\varnothing \in \mathrm{Haus}$$
10	8 9	ax-mp	$$⊢𝒫\varnothing \in \mathrm{Haus}$$
11	7 10	eqeltri	$$⊢1_{𝑜}\in \mathrm{Haus}$$
12		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
13		pwpw0	$$⊢𝒫\left\{\varnothing \right\}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
14	12 13	eqtr4i	$$⊢2_{𝑜}=𝒫\left\{\varnothing \right\}$$
15		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
16		dishaus	$$⊢\left\{\varnothing \right\}\in \mathrm{V}\to 𝒫\left\{\varnothing \right\}\in \mathrm{Haus}$$
17	15 16	ax-mp	$$⊢𝒫\left\{\varnothing \right\}\in \mathrm{Haus}$$
18	14 17	eqeltri	$$⊢2_{𝑜}\in \mathrm{Haus}$$
19		prssi	$$⊢\left(1_{𝑜}\in \mathrm{Haus}\wedge 2_{𝑜}\in \mathrm{Haus}\right)\to \left\{1_{𝑜},2_{𝑜}\right\}\subseteq \mathrm{Haus}$$
20	11 18 19	mp2an	$$⊢\left\{1_{𝑜},2_{𝑜}\right\}\subseteq \mathrm{Haus}$$
21	4 20	ssini	$$⊢\left\{1_{𝑜},2_{𝑜}\right\}\subseteq \mathrm{On}\cap \mathrm{Haus}$$