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	|- { (/) , A } e. Conn

Proof

Step	Hyp	Ref	Expression
1		indistop	|- { (/) , A } e. Top
2		inss1	|- ( { (/) , A } i^i ( Clsd ` { (/) , A } ) ) C_ { (/) , A }
3		indislem	|- { (/) , ( _I ` A ) } = { (/) , A }
4	2 3	sseqtrri	|- ( { (/) , A } i^i ( Clsd ` { (/) , A } ) ) C_ { (/) , ( _I ` A ) }
5		indisuni	|- ( _I ` A ) = U. { (/) , A }
6	5	isconn2	|- ( { (/) , A } e. Conn <-> ( { (/) , A } e. Top /\ ( { (/) , A } i^i ( Clsd ` { (/) , A } ) ) C_ { (/) , ( _I ` A ) } ) )
7	1 4 6	mpbir2an	|- { (/) , A } e. Conn