Definition df-conn 22263

Description: Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.)

Assertion

Ref	Expression
df-conn	⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}

Detailed syntax breakdown of Definition df-conn

Step	Hyp	Ref	Expression
1		cconn 22262	. 2 class Conn
2		vj	. . . . . 6 setvar 𝑗
3	2	cv 1542	. . . . 5 class 𝑗
4		ccld 21867	. . . . . 6 class Clsd
5	3, 4	cfv 6358	. . . . 5 class (Clsd‘𝑗)
6	3, 5	cin 3852	. . . 4 class (𝑗 ∩ (Clsd‘𝑗))
7		c0 4223	. . . . 5 class ∅
8	3	cuni 4805	. . . . 5 class ∪ 𝑗
9	7, 8	cpr 4529	. . . 4 class {∅, ∪ 𝑗}
10	6, 9	wceq 1543	. . 3 wff (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}
11		ctop 21744	. . 3 class Top
12	10, 2, 11	crab 3055	. 2 class {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}
13	1, 12	wceq 1543	1 wff Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}

This definition is referenced by:  isconn  22264