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	$$⊢\mathrm{Conn}=\left\{j\in \mathrm{Top}|j\cap \mathrm{Clsd}\left(j\right)=\left\{\varnothing ,\bigcup j\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cconn	$$class\mathrm{Conn}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3	1	cv	$$setvarj$$
4		ccld	$$class\mathrm{Clsd}$$
5	3 4	cfv	$$class\mathrm{Clsd}\left(j\right)$$
6	3 5	cin	$$class\left(j\cap \mathrm{Clsd}\left(j\right)\right)$$
7		c0	$$class\varnothing$$
8	3	cuni	$$class\bigcup j$$
9	7 8	cpr	$$class\left\{\varnothing ,\bigcup j\right\}$$
10	6 9	wceq	$$wffj\cap \mathrm{Clsd}\left(j\right)=\left\{\varnothing ,\bigcup j\right\}$$
11	10 1 2	crab	$$class\left\{j\in \mathrm{Top}|j\cap \mathrm{Clsd}\left(j\right)=\left\{\varnothing ,\bigcup j\right\}\right\}$$
12	0 11	wceq	$$wff\mathrm{Conn}=\left\{j\in \mathrm{Top}|j\cap \mathrm{Clsd}\left(j\right)=\left\{\varnothing ,\bigcup j\right\}\right\}$$