Metamath Proof Explorer


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=jTop|jClsdj=j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconn classConn
1 vj setvarj
2 ctop classTop
3 1 cv setvarj
4 ccld classClsd
5 3 4 cfv classClsdj
6 3 5 cin classjClsdj
7 c0 class
8 3 cuni classj
9 7 8 cpr classj
10 6 9 wceq wffjClsdj=j
11 10 1 2 crab classjTop|jClsdj=j
12 0 11 wceq wffConn=jTop|jClsdj=j