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	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( { ∅ , 𝑋 } ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2		0opn	⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
3	1 2	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∅ ∈ 𝐽 )
4		toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
5	3 4	prssd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → { ∅ , 𝑋 } ⊆ 𝐽 )
6		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7		eqimss2	⊢ ( 𝑋 = ∪ 𝐽 → ∪ 𝐽 ⊆ 𝑋 )
8	6 7	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∪ 𝐽 ⊆ 𝑋 )
9		sspwuni	⊢ ( 𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋 )
10	8 9	sylibr	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ⊆ 𝒫 𝑋 )
11	5 10	jca	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( { ∅ , 𝑋 } ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋 ) )