conncompcld

Description: The connected component containing A is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Hypothesis	conncomp.2	$⊢ S = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
	Assertion	conncompcld	$⊢ (J \in TopOn (X) \land A \in X) \to S \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	$⊢ S = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
2		topontop	$⊢ J \in TopOn (X) \to J \in Top$
3		ssrab2	$⊢ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq 𝒫 X$
4		sspwuni	$⊢ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq 𝒫 X \leftrightarrow ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq X$
5	3 4	mpbi	$⊢ ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \subseteq X$
6	1 5	eqsstri	$⊢ S \subseteq X$
7		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
8	7	adantr	$⊢ (J \in TopOn (X) \land A \in X) \to X = ⋃ J$
9	6 8	sseqtrid	$⊢ (J \in TopOn (X) \land A \in X) \to S \subseteq ⋃ J$
10		eqid	$⊢ ⋃ J = ⋃ J$
11	10	clsss3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \subseteq ⋃ J$
12	2 9 11	syl2an2r	$⊢ (J \in TopOn (X) \land A \in X) \to cls (J) (S) \subseteq ⋃ J$
13	12 8	sseqtrrd	$⊢ (J \in TopOn (X) \land A \in X) \to cls (J) (S) \subseteq X$
14	10	sscls	$⊢ (J \in Top \land S \subseteq ⋃ J) \to S \subseteq cls (J) (S)$
15	2 9 14	syl2an2r	$⊢ (J \in TopOn (X) \land A \in X) \to S \subseteq cls (J) (S)$
16	1	conncompid	$⊢ (J \in TopOn (X) \land A \in X) \to A \in S$
17	15 16	sseldd	$⊢ (J \in TopOn (X) \land A \in X) \to A \in cls (J) (S)$
18		simpl	$⊢ (J \in TopOn (X) \land A \in X) \to J \in TopOn (X)$
19	6	a1i	$⊢ (J \in TopOn (X) \land A \in X) \to S \subseteq X$
20	1	conncompconn	$⊢ (J \in TopOn (X) \land A \in X) \to J ↾_{𝑡} S \in Conn$
21		clsconn	$⊢ (J \in TopOn (X) \land S \subseteq X \land J ↾_{𝑡} S \in Conn) \to J ↾_{𝑡} cls (J) (S) \in Conn$
22	18 19 20 21	syl3anc	$⊢ (J \in TopOn (X) \land A \in X) \to J ↾_{𝑡} cls (J) (S) \in Conn$
23	1	conncompss	$⊢ (cls (J) (S) \subseteq X \land A \in cls (J) (S) \land J ↾_{𝑡} cls (J) (S) \in Conn) \to cls (J) (S) \subseteq S$
24	13 17 22 23	syl3anc	$⊢ (J \in TopOn (X) \land A \in X) \to cls (J) (S) \subseteq S$
25	10	iscld4	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) \subseteq S)$
26	2 9 25	syl2an2r	$⊢ (J \in TopOn (X) \land A \in X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) \subseteq S)$
27	24 26	mpbird	$⊢ (J \in TopOn (X) \land A \in X) \to S \in Clsd (J)$

Metamath Proof Explorer

Theorem conncompcld

Proof