This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )