Metamath Proof Explorer


Theorem indisconn

Description: The indiscrete topology (or trivial topology) on any set is connected. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion indisconn { ∅ , 𝐴 } ∈ Conn

Proof

Step Hyp Ref Expression
1 indistop { ∅ , 𝐴 } ∈ Top
2 inss1 ( { ∅ , 𝐴 } ∩ ( Clsd ‘ { ∅ , 𝐴 } ) ) ⊆ { ∅ , 𝐴 }
3 indislem { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }
4 2 3 sseqtrri ( { ∅ , 𝐴 } ∩ ( Clsd ‘ { ∅ , 𝐴 } ) ) ⊆ { ∅ , ( I ‘ 𝐴 ) }
5 indisuni ( I ‘ 𝐴 ) = { ∅ , 𝐴 }
6 5 isconn2 ( { ∅ , 𝐴 } ∈ Conn ↔ ( { ∅ , 𝐴 } ∈ Top ∧ ( { ∅ , 𝐴 } ∩ ( Clsd ‘ { ∅ , 𝐴 } ) ) ⊆ { ∅ , ( I ‘ 𝐴 ) } ) )
7 1 4 6 mpbir2an { ∅ , 𝐴 } ∈ Conn