conncompclo

Description: The connected component containing A is a subset of any clopen set containing A . (Contributed by Mario Carneiro, 20-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	$⊢ S = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
2		eqid	$⊢ ⋃ J = ⋃ J$
3		simp1	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to J \in TopOn (X)$
4		simp2	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to T \in (J \cap Clsd (J))$
5	4	elin1d	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to T \in J$
6		toponss	$⊢ (J \in TopOn (X) \land T \in J) \to T \subseteq X$
7	3 5 6	syl2anc	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to T \subseteq X$
8		simp3	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to A \in T$
9	7 8	sseldd	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to A \in X$
10	1	conncompcld	$⊢ (J \in TopOn (X) \land A \in X) \to S \in Clsd (J)$
11	3 9 10	syl2anc	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to S \in Clsd (J)$
12	2	cldss	$⊢ S \in Clsd (J) \to S \subseteq ⋃ J$
13	11 12	syl	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to S \subseteq ⋃ J$
14	1	conncompconn	$⊢ (J \in TopOn (X) \land A \in X) \to J ↾_{𝑡} S \in Conn$
15	3 9 14	syl2anc	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to J ↾_{𝑡} S \in Conn$
16	1	conncompid	$⊢ (J \in TopOn (X) \land A \in X) \to A \in S$
17	3 9 16	syl2anc	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to A \in S$
18		inelcm	$⊢ (A \in T \land A \in S) \to T \cap S \neq \emptyset$
19	8 17 18	syl2anc	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to T \cap S \neq \emptyset$
20	4	elin2d	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to T \in Clsd (J)$
21	2 13 15 5 19 20	connsubclo	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land A \in T) \to S \subseteq T$

Metamath Proof Explorer

Theorem conncompclo

Proof