Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
1
|
cldss |
|- ( B e. ( Clsd ` J ) -> B C_ U. J ) |
3 |
|
dfss4 |
|- ( B C_ U. J <-> ( U. J \ ( U. J \ B ) ) = B ) |
4 |
2 3
|
sylib |
|- ( B e. ( Clsd ` J ) -> ( U. J \ ( U. J \ B ) ) = B ) |
5 |
4
|
ralimi |
|- ( A. x e. A B e. ( Clsd ` J ) -> A. x e. A ( U. J \ ( U. J \ B ) ) = B ) |
6 |
|
iineq2 |
|- ( A. x e. A ( U. J \ ( U. J \ B ) ) = B -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = |^|_ x e. A B ) |
7 |
5 6
|
syl |
|- ( A. x e. A B e. ( Clsd ` J ) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = |^|_ x e. A B ) |
8 |
7
|
adantl |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = |^|_ x e. A B ) |
9 |
|
iindif2 |
|- ( A =/= (/) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = ( U. J \ U_ x e. A ( U. J \ B ) ) ) |
10 |
9
|
adantr |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A ( U. J \ ( U. J \ B ) ) = ( U. J \ U_ x e. A ( U. J \ B ) ) ) |
11 |
8 10
|
eqtr3d |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B = ( U. J \ U_ x e. A ( U. J \ B ) ) ) |
12 |
|
r19.2z |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> E. x e. A B e. ( Clsd ` J ) ) |
13 |
|
cldrcl |
|- ( B e. ( Clsd ` J ) -> J e. Top ) |
14 |
13
|
rexlimivw |
|- ( E. x e. A B e. ( Clsd ` J ) -> J e. Top ) |
15 |
12 14
|
syl |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> J e. Top ) |
16 |
1
|
cldopn |
|- ( B e. ( Clsd ` J ) -> ( U. J \ B ) e. J ) |
17 |
16
|
ralimi |
|- ( A. x e. A B e. ( Clsd ` J ) -> A. x e. A ( U. J \ B ) e. J ) |
18 |
17
|
adantl |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> A. x e. A ( U. J \ B ) e. J ) |
19 |
|
iunopn |
|- ( ( J e. Top /\ A. x e. A ( U. J \ B ) e. J ) -> U_ x e. A ( U. J \ B ) e. J ) |
20 |
15 18 19
|
syl2anc |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> U_ x e. A ( U. J \ B ) e. J ) |
21 |
1
|
opncld |
|- ( ( J e. Top /\ U_ x e. A ( U. J \ B ) e. J ) -> ( U. J \ U_ x e. A ( U. J \ B ) ) e. ( Clsd ` J ) ) |
22 |
15 20 21
|
syl2anc |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> ( U. J \ U_ x e. A ( U. J \ B ) ) e. ( Clsd ` J ) ) |
23 |
11 22
|
eqeltrd |
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B e. ( Clsd ` J ) ) |