Metamath Proof Explorer

Theorem conncompconn

Description: The connected component containing A is connected. (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	conncompconn	$⊢ (J \in TopOn (X) \land A \in X) \to J ↾_{𝑡} S \in Conn$

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	$⊢ S = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
2		uniiun	$⊢ ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} = ⋃_{y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}} y$
3	1 2	eqtri	$⊢ S = ⋃_{y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}} y$
4	3	oveq2i	$⊢ J ↾_{𝑡} S = J ↾_{𝑡} ⋃_{y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}} y$
5		simpl	$⊢ (J \in TopOn (X) \land A \in X) \to J \in TopOn (X)$
6		simpr	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
7		eleq2w	$⊢ x = y \to (A \in x \leftrightarrow A \in y)$
8		oveq2	$⊢ x = y \to J ↾_{𝑡} x = J ↾_{𝑡} y$
9	8	eleq1d	$⊢ x = y \to (J ↾_{𝑡} x \in Conn \leftrightarrow J ↾_{𝑡} y \in Conn)$
10	7 9	anbi12d	$⊢ x = y \to ((A \in x \land J ↾_{𝑡} x \in Conn) \leftrightarrow (A \in y \land J ↾_{𝑡} y \in Conn))$
11	10	elrab	$⊢ y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \leftrightarrow (y \in 𝒫 X \land (A \in y \land J ↾_{𝑡} y \in Conn))$
12	6 11	sylib	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to (y \in 𝒫 X \land (A \in y \land J ↾_{𝑡} y \in Conn))$
13	12	simpld	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to y \in 𝒫 X$
14	13	elpwid	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to y \subseteq X$
15	12	simprd	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to (A \in y \land J ↾_{𝑡} y \in Conn)$
16	15	simpld	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to A \in y$
17	15	simprd	$⊢ ((J \in TopOn (X) \land A \in X) \land y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}) \to J ↾_{𝑡} y \in Conn$
18	5 14 16 17	iunconn	$⊢ (J \in TopOn (X) \land A \in X) \to J ↾_{𝑡} ⋃_{y \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}} y \in Conn$
19	4 18	eqeltrid	$⊢ (J \in TopOn (X) \land A \in X) \to J ↾_{𝑡} S \in Conn$