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 = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
	Assertion	conncompss	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to T \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	$⊢ S = ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
2		simp1	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to T \subseteq X$
3		conntop	$⊢ J ↾_{𝑡} T \in Conn \to J ↾_{𝑡} T \in Top$
4	3	3ad2ant3	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to J ↾_{𝑡} T \in Top$
5		restrcl	$⊢ J ↾_{𝑡} T \in Top \to (J \in V \land T \in V)$
6	5	simprd	$⊢ J ↾_{𝑡} T \in Top \to T \in V$
7		elpwg	$⊢ T \in V \to (T \in 𝒫 X \leftrightarrow T \subseteq X)$
8	4 6 7	3syl	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to (T \in 𝒫 X \leftrightarrow T \subseteq X)$
9	2 8	mpbird	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to T \in 𝒫 X$
10		3simpc	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to (A \in T \land J ↾_{𝑡} T \in Conn)$
11		eleq2	$⊢ y = T \to (A \in y \leftrightarrow A \in T)$
12		oveq2	$⊢ y = T \to J ↾_{𝑡} y = J ↾_{𝑡} T$
13	12	eleq1d	$⊢ y = T \to (J ↾_{𝑡} y \in Conn \leftrightarrow J ↾_{𝑡} T \in Conn)$
14	11 13	anbi12d	$⊢ y = T \to ((A \in y \land J ↾_{𝑡} y \in Conn) \leftrightarrow (A \in T \land J ↾_{𝑡} T \in Conn))$
15		eleq2	$⊢ x = y \to (A \in x \leftrightarrow A \in y)$
16		oveq2	$⊢ x = y \to J ↾_{𝑡} x = J ↾_{𝑡} y$
17	16	eleq1d	$⊢ x = y \to (J ↾_{𝑡} x \in Conn \leftrightarrow J ↾_{𝑡} y \in Conn)$
18	15 17	anbi12d	$⊢ x = y \to ((A \in x \land J ↾_{𝑡} x \in Conn) \leftrightarrow (A \in y \land J ↾_{𝑡} y \in Conn))$
19	18	cbvrabv	$⊢ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} = \{y \in 𝒫 X \| (A \in y \land J ↾_{𝑡} y \in Conn)\}$
20	14 19	elrab2	$⊢ T \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \leftrightarrow (T \in 𝒫 X \land (A \in T \land J ↾_{𝑡} T \in Conn))$
21	9 10 20	sylanbrc	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to T \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
22		elssuni	$⊢ T \in \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\} \to T \subseteq ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
23	21 22	syl	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to T \subseteq ⋃ \{x \in 𝒫 X \| (A \in x \land J ↾_{𝑡} x \in Conn)\}$
24	23 1	sseqtrrdi	$⊢ (T \subseteq X \land A \in T \land J ↾_{𝑡} T \in Conn) \to T \subseteq S$

Metamath Proof Explorer

Theorem conncompss

Proof