Step |
Hyp |
Ref |
Expression |
1 |
|
isconn.1 |
|- X = U. J |
2 |
1
|
isconn |
|- ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) ) |
3 |
|
eqss |
|- ( ( J i^i ( Clsd ` J ) ) = { (/) , X } <-> ( ( J i^i ( Clsd ` J ) ) C_ { (/) , X } /\ { (/) , X } C_ ( J i^i ( Clsd ` J ) ) ) ) |
4 |
|
0opn |
|- ( J e. Top -> (/) e. J ) |
5 |
|
0cld |
|- ( J e. Top -> (/) e. ( Clsd ` J ) ) |
6 |
4 5
|
elind |
|- ( J e. Top -> (/) e. ( J i^i ( Clsd ` J ) ) ) |
7 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
8 |
1
|
topcld |
|- ( J e. Top -> X e. ( Clsd ` J ) ) |
9 |
7 8
|
elind |
|- ( J e. Top -> X e. ( J i^i ( Clsd ` J ) ) ) |
10 |
6 9
|
prssd |
|- ( J e. Top -> { (/) , X } C_ ( J i^i ( Clsd ` J ) ) ) |
11 |
10
|
biantrud |
|- ( J e. Top -> ( ( J i^i ( Clsd ` J ) ) C_ { (/) , X } <-> ( ( J i^i ( Clsd ` J ) ) C_ { (/) , X } /\ { (/) , X } C_ ( J i^i ( Clsd ` J ) ) ) ) ) |
12 |
3 11
|
bitr4id |
|- ( J e. Top -> ( ( J i^i ( Clsd ` J ) ) = { (/) , X } <-> ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) ) |
13 |
12
|
pm5.32i |
|- ( ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) ) |
14 |
2 13
|
bitri |
|- ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) C_ { (/) , X } ) ) |