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