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 = { 𝑗 ∈ Top ∣ ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = { ∅ , ∪ 𝑗 } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cconn	⊢ Conn
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3	1	cv	⊢ 𝑗
4		ccld	⊢ Clsd
5	3 4	cfv	⊢ ( Clsd ‘ 𝑗 )
6	3 5	cin	⊢ ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) )
7		c0	⊢ ∅
8	3	cuni	⊢ ∪ 𝑗
9	7 8	cpr	⊢ { ∅ , ∪ 𝑗 }
10	6 9	wceq	⊢ ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = { ∅ , ∪ 𝑗 }
11	10 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = { ∅ , ∪ 𝑗 } }
12	0 11	wceq	⊢ Conn = { 𝑗 ∈ Top ∣ ( 𝑗 ∩ ( Clsd ‘ 𝑗 ) ) = { ∅ , ∪ 𝑗 } }