Theorem topgele

Description: The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010) (Revised by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Assertion	topgele	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \left(\left\{\varnothing ,X\right\}\subseteq J\wedge J\subseteq 𝒫X\right)$$

Proof

Step	Hyp	Ref	Expression
1		topontop	$$⊢J\in \mathrm{TopOn}\left(X\right)\to J\in \mathrm{Top}$$
2		0opn	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$
3	1 2	syl	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \varnothing \in J$$
4		toponmax	$$⊢J\in \mathrm{TopOn}\left(X\right)\to X\in J$$
5	3 4	prssd	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \left\{\varnothing ,X\right\}\subseteq J$$
6		toponuni	$$⊢J\in \mathrm{TopOn}\left(X\right)\to X=\bigcup J$$
7		eqimss2	$$⊢X=\bigcup J\to \bigcup J\subseteq X$$
8	6 7	syl	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \bigcup J\subseteq X$$
9		sspwuni	$$⊢J\subseteq 𝒫X\leftrightarrow \bigcup J\subseteq X$$
10	8 9	sylibr	$$⊢J\in \mathrm{TopOn}\left(X\right)\to J\subseteq 𝒫X$$
11	5 10	jca	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \left(\left\{\varnothing ,X\right\}\subseteq J\wedge J\subseteq 𝒫X\right)$$