Theorem conncompss

Description: The connected component containing A is a superset of any other connected set containing A . (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	conncompss	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T C_ S )

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	|- S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
2		simp1	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T C_ X )
3		conntop	|- ( ( J |`t T ) e. Conn -> ( J |`t T ) e. Top )
4	3	3ad2ant3	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> ( J |`t T ) e. Top )
5		restrcl	|- ( ( J |`t T ) e. Top -> ( J e. _V /\ T e. _V ) )
6	5	simprd	|- ( ( J |`t T ) e. Top -> T e. _V )
7		elpwg	|- ( T e. _V -> ( T e. ~P X <-> T C_ X ) )
8	4 6 7	3syl	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> ( T e. ~P X <-> T C_ X ) )
9	2 8	mpbird	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T e. ~P X )
10		3simpc	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> ( A e. T /\ ( J |`t T ) e. Conn ) )
11		eleq2	|- ( y = T -> ( A e. y <-> A e. T ) )
12		oveq2	|- ( y = T -> ( J |`t y ) = ( J |`t T ) )
13	12	eleq1d	|- ( y = T -> ( ( J |`t y ) e. Conn <-> ( J |`t T ) e. Conn ) )
14	11 13	anbi12d	|- ( y = T -> ( ( A e. y /\ ( J |`t y ) e. Conn ) <-> ( A e. T /\ ( J |`t T ) e. Conn ) ) )
15		eleq2	|- ( x = y -> ( A e. x <-> A e. y ) )
16		oveq2	|- ( x = y -> ( J |`t x ) = ( J |`t y ) )
17	16	eleq1d	|- ( x = y -> ( ( J |`t x ) e. Conn <-> ( J |`t y ) e. Conn ) )
18	15 17	anbi12d	|- ( x = y -> ( ( A e. x /\ ( J |`t x ) e. Conn ) <-> ( A e. y /\ ( J |`t y ) e. Conn ) ) )
19	18	cbvrabv	|- { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } = { y e. ~P X | ( A e. y /\ ( J |`t y ) e. Conn ) }
20	14 19	elrab2	|- ( T e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } <-> ( T e. ~P X /\ ( A e. T /\ ( J |`t T ) e. Conn ) ) )
21	9 10 20	sylanbrc	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )
22		elssuni	|- ( T e. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } -> T C_ U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )
23	21 22	syl	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T C_ U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )
24	23 1	sseqtrrdi	|- ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T C_ S )