Step |
Hyp |
Ref |
Expression |
1 |
|
conncomp.2 |
|- S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } |
2 |
|
uniiun |
|- U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } = U_ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y |
3 |
1 2
|
eqtri |
|- S = U_ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y |
4 |
3
|
oveq2i |
|- ( J |`t S ) = ( J |`t U_ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y ) |
5 |
|
simpl |
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> J e. ( TopOn ` X ) ) |
6 |
|
simpr |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) |
7 |
|
eleq2w |
|- ( x = y -> ( A e. x <-> A e. y ) ) |
8 |
|
oveq2 |
|- ( x = y -> ( J |`t x ) = ( J |`t y ) ) |
9 |
8
|
eleq1d |
|- ( x = y -> ( ( J |`t x ) e. Conn <-> ( J |`t y ) e. Conn ) ) |
10 |
7 9
|
anbi12d |
|- ( x = y -> ( ( A e. x /\ ( J |`t x ) e. Conn ) <-> ( A e. y /\ ( J |`t y ) e. Conn ) ) ) |
11 |
10
|
elrab |
|- ( y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } <-> ( y e. ~P X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) |
12 |
6 11
|
sylib |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> ( y e. ~P X /\ ( A e. y /\ ( J |`t y ) e. Conn ) ) ) |
13 |
12
|
simpld |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> y e. ~P X ) |
14 |
13
|
elpwid |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> y C_ X ) |
15 |
12
|
simprd |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> ( A e. y /\ ( J |`t y ) e. Conn ) ) |
16 |
15
|
simpld |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> A e. y ) |
17 |
15
|
simprd |
|- ( ( ( J e. ( TopOn ` X ) /\ A e. X ) /\ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } ) -> ( J |`t y ) e. Conn ) |
18 |
5 14 16 17
|
iunconn |
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t U_ y e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } y ) e. Conn ) |
19 |
4 18
|
eqeltrid |
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t S ) e. Conn ) |