conncompcld

Description: The connected component containing A is a closed set. (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	conncompcld	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	\|- S = U. { x e. ~P X \| ( A e. x /\ ( J \|`t x ) e. Conn ) }
2		topontop	\|- ( J e. ( TopOn ` X ) -> J e. Top )
3		ssrab2	\|- { x e. ~P X \| ( A e. x /\ ( J \|`t x ) e. Conn ) } C_ ~P X
4		sspwuni	\|- ( { x e. ~P X \| ( A e. x /\ ( J \|`t x ) e. Conn ) } C_ ~P X <-> U. { x e. ~P X \| ( A e. x /\ ( J \|`t x ) e. Conn ) } C_ X )
5	3 4	mpbi	\|- U. { x e. ~P X \| ( A e. x /\ ( J \|`t x ) e. Conn ) } C_ X
6	1 5	eqsstri	\|- S C_ X
7		toponuni	\|- ( J e. ( TopOn ` X ) -> X = U. J )
8	7	adantr	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> X = U. J )
9	6 8	sseqtrid	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S C_ U. J )
10		eqid	\|- U. J = U. J
11	10	clsss3	\|- ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
12	2 9 11	syl2an2r	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( cls ` J ) ` S ) C_ U. J )
13	12 8	sseqtrrd	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( cls ` J ) ` S ) C_ X )
14	10	sscls	\|- ( ( J e. Top /\ S C_ U. J ) -> S C_ ( ( cls ` J ) ` S ) )
15	2 9 14	syl2an2r	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S C_ ( ( cls ` J ) ` S ) )
16	1	conncompid	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. S )
17	15 16	sseldd	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. ( ( cls ` J ) ` S ) )
18		simpl	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> J e. ( TopOn ` X ) )
19	6	a1i	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S C_ X )
20	1	conncompconn	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J \|`t S ) e. Conn )
21		clsconn	\|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ ( J \|`t S ) e. Conn ) -> ( J \|`t ( ( cls ` J ) ` S ) ) e. Conn )
22	18 19 20 21	syl3anc	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J \|`t ( ( cls ` J ) ` S ) ) e. Conn )
23	1	conncompss	\|- ( ( ( ( cls ` J ) ` S ) C_ X /\ A e. ( ( cls ` J ) ` S ) /\ ( J \|`t ( ( cls ` J ) ` S ) ) e. Conn ) -> ( ( cls ` J ) ` S ) C_ S )
24	13 17 22 23	syl3anc	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( cls ` J ) ` S ) C_ S )
25	10	iscld4	\|- ( ( J e. Top /\ S C_ U. J ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
26	2 9 25	syl2an2r	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
27	24 26	mpbird	\|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S e. ( Clsd ` J ) )

Metamath Proof Explorer

Theorem conncompcld

Proof