Definition df-conn 21215

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

Assertion

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

Detailed syntax breakdown of Definition df-conn

Step	Hyp	Ref	Expression
1		cconn 21214	. 2 class Conn
2		vj	. . . . . 6 setvar j
3	2	cv 1482	. . . . 5 class j
4		ccld 20820	. . . . . 6 class Clsd
5	3, 4	cfv 5888	. . . . 5 class ( Clsd ` j )
6	3, 5	cin 3573	. . . 4 class ( j i^i ( Clsd ` j ) )
7		c0 3915	. . . . 5 class (/)
8	3	cuni 4436	. . . . 5 class U. j
9	7, 8	cpr 4179	. . . 4 class { (/) , U. j }
10	6, 9	wceq 1483	. . 3 wff ( j i^i ( Clsd ` j ) ) = { (/) , U. j }
11		ctop 20698	. . 3 class Top
12	10, 2, 11	crab 2916	. 2 class { j e. Top | ( j i^i ( Clsd ` j ) ) = { (/) , U. j } }
13	1, 12	wceq 1483	1 wff Conn = { j e. Top | ( j i^i ( Clsd ` j ) ) = { (/) , U. j } }

This definition is referenced by:  isconn  21216