Step |
Hyp |
Ref |
Expression |
1 |
|
iscld.1 |
|- X = U. J |
2 |
1
|
ntrfval |
|- ( J e. Top -> ( int ` J ) = ( x e. ~P X |-> U. ( J i^i ~P x ) ) ) |
3 |
2
|
fveq1d |
|- ( J e. Top -> ( ( int ` J ) ` S ) = ( ( x e. ~P X |-> U. ( J i^i ~P x ) ) ` S ) ) |
4 |
3
|
adantr |
|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = ( ( x e. ~P X |-> U. ( J i^i ~P x ) ) ` S ) ) |
5 |
|
eqid |
|- ( x e. ~P X |-> U. ( J i^i ~P x ) ) = ( x e. ~P X |-> U. ( J i^i ~P x ) ) |
6 |
|
pweq |
|- ( x = S -> ~P x = ~P S ) |
7 |
6
|
ineq2d |
|- ( x = S -> ( J i^i ~P x ) = ( J i^i ~P S ) ) |
8 |
7
|
unieqd |
|- ( x = S -> U. ( J i^i ~P x ) = U. ( J i^i ~P S ) ) |
9 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
10 |
|
elpw2g |
|- ( X e. J -> ( S e. ~P X <-> S C_ X ) ) |
11 |
9 10
|
syl |
|- ( J e. Top -> ( S e. ~P X <-> S C_ X ) ) |
12 |
11
|
biimpar |
|- ( ( J e. Top /\ S C_ X ) -> S e. ~P X ) |
13 |
|
inex1g |
|- ( J e. Top -> ( J i^i ~P S ) e. _V ) |
14 |
13
|
adantr |
|- ( ( J e. Top /\ S C_ X ) -> ( J i^i ~P S ) e. _V ) |
15 |
14
|
uniexd |
|- ( ( J e. Top /\ S C_ X ) -> U. ( J i^i ~P S ) e. _V ) |
16 |
5 8 12 15
|
fvmptd3 |
|- ( ( J e. Top /\ S C_ X ) -> ( ( x e. ~P X |-> U. ( J i^i ~P x ) ) ` S ) = U. ( J i^i ~P S ) ) |
17 |
4 16
|
eqtrd |
|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) ) |