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