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		eleq2w	|- ( x = y -> ( A e. x <-> A e. y ) )
7		oveq2	|- ( x = y -> ( J |`t x ) = ( J |`t y ) )
8	7	eleq1d	|- ( x = y -> ( ( J |`t x ) e. Conn <-> ( J |`t y ) e. Conn ) )
9	6 8	anbi12d	|- ( x = y -> ( ( A e. x /\ ( J |`t x ) e. Conn ) <-> ( A e. y /\ ( J |`t y ) e. Conn ) ) )
10	9	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 ) ) )
11	10	bilani	|- ( ( ( 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 ) ) )
12	11	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 )
13	12	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 )
14	11	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 ) )
15	14	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 )
16	14	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 )
17	5 13 15 16	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 )
18	4 17	eqeltrid	|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t S ) e. Conn )