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 )

Metamath Proof Explorer

Theorem conncompss

Proof