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 \in Top \| j \cap Clsd (j) = \{\emptyset, ⋃ j\}\}$

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

Metamath Proof Explorer