Metamath Proof Explorer


Theorem conncompconn

Description: The connected component containing A is connected. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypothesis conncomp.2
|- S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
Assertion conncompconn
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t S ) e. Conn )

Proof

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 )