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