This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 TopOn (X) \to (\{\emptyset, X\} \subseteq J \land J \subseteq 𝒫 X)$

Proof

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