| Step |
Hyp |
Ref |
Expression |
| 1 |
|
connsubclo.1 |
|- X = U. J |
| 2 |
|
connsubclo.3 |
|- ( ph -> A C_ X ) |
| 3 |
|
connsubclo.4 |
|- ( ph -> ( J |`t A ) e. Conn ) |
| 4 |
|
connsubclo.5 |
|- ( ph -> B e. J ) |
| 5 |
|
connsubclo.6 |
|- ( ph -> ( B i^i A ) =/= (/) ) |
| 6 |
|
connsubclo.7 |
|- ( ph -> B e. ( Clsd ` J ) ) |
| 7 |
|
eqid |
|- U. ( J |`t A ) = U. ( J |`t A ) |
| 8 |
|
cldrcl |
|- ( B e. ( Clsd ` J ) -> J e. Top ) |
| 9 |
6 8
|
syl |
|- ( ph -> J e. Top ) |
| 10 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
| 11 |
9 10
|
syl |
|- ( ph -> X e. J ) |
| 12 |
11 2
|
ssexd |
|- ( ph -> A e. _V ) |
| 13 |
|
elrestr |
|- ( ( J e. Top /\ A e. _V /\ B e. J ) -> ( B i^i A ) e. ( J |`t A ) ) |
| 14 |
9 12 4 13
|
syl3anc |
|- ( ph -> ( B i^i A ) e. ( J |`t A ) ) |
| 15 |
|
eqid |
|- ( B i^i A ) = ( B i^i A ) |
| 16 |
|
ineq1 |
|- ( x = B -> ( x i^i A ) = ( B i^i A ) ) |
| 17 |
16
|
rspceeqv |
|- ( ( B e. ( Clsd ` J ) /\ ( B i^i A ) = ( B i^i A ) ) -> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) ) |
| 18 |
6 15 17
|
sylancl |
|- ( ph -> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) ) |
| 19 |
1
|
restcld |
|- ( ( J e. Top /\ A C_ X ) -> ( ( B i^i A ) e. ( Clsd ` ( J |`t A ) ) <-> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) ) ) |
| 20 |
9 2 19
|
syl2anc |
|- ( ph -> ( ( B i^i A ) e. ( Clsd ` ( J |`t A ) ) <-> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) ) ) |
| 21 |
18 20
|
mpbird |
|- ( ph -> ( B i^i A ) e. ( Clsd ` ( J |`t A ) ) ) |
| 22 |
7 3 14 5 21
|
connclo |
|- ( ph -> ( B i^i A ) = U. ( J |`t A ) ) |
| 23 |
1
|
restuni |
|- ( ( J e. Top /\ A C_ X ) -> A = U. ( J |`t A ) ) |
| 24 |
9 2 23
|
syl2anc |
|- ( ph -> A = U. ( J |`t A ) ) |
| 25 |
22 24
|
eqtr4d |
|- ( ph -> ( B i^i A ) = A ) |
| 26 |
|
sseqin2 |
|- ( A C_ B <-> ( B i^i A ) = A ) |
| 27 |
25 26
|
sylibr |
|- ( ph -> A C_ B ) |