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 |
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 |