Definition df-conn

Description: Topologies are connected when only (/) and U. j are both open and closed. (Contributed by FL, 17-Nov-2008)

	Ref	Expression
Assertion	df-conn	|- Conn = { j e. Top | ( j i^i ( Clsd ` j ) ) = { (/) , U. j } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cconn	|- Conn
1		vj	|- j
2		ctop	|- Top
3	1	cv	|- j
4		ccld	|- Clsd
5	3 4	cfv	|- ( Clsd ` j )
6	3 5	cin	|- ( j i^i ( Clsd ` j ) )
7		c0	|- (/)
8	3	cuni	|- U. j
9	7 8	cpr	|- { (/) , U. j }
10	6 9	wceq	|- ( j i^i ( Clsd ` j ) ) = { (/) , U. j }
11	10 1 2	crab	|- { j e. Top | ( j i^i ( Clsd ` j ) ) = { (/) , U. j } }
12	0 11	wceq	|- Conn = { j e. Top | ( j i^i ( Clsd ` j ) ) = { (/) , U. j } }