tgpconncompss

Description: The identity component is a subset of any open subgroup. (Contributed by Mario Carneiro, 17-Sep-2015)

	Ref	Expression
Hypotheses	tgpconncomp.x	$⊢ X = {Base}_{G}$
	tgpconncomp.z	$⊢ \underset{˙}{0} = 0_{G}$
	tgpconncomp.j	$⊢ J = TopOpen (G)$
	tgpconncomp.s	$⊢ S = ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\}$
Assertion	tgpconncompss	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to S \subseteq T$

Step	Hyp	Ref	Expression
1		tgpconncomp.x	$⊢ X = {Base}_{G}$
2		tgpconncomp.z	$⊢ \underset{˙}{0} = 0_{G}$
3		tgpconncomp.j	$⊢ J = TopOpen (G)$
4		tgpconncomp.s	$⊢ S = ⋃ \{x \in 𝒫 X \| (\underset{˙}{0} \in x \land J ↾_{𝑡} x \in Conn)\}$
5	3 1	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (X)$
6	5	3ad2ant1	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to J \in TopOn (X)$
7		simp3	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to T \in J$
8	3	opnsubg	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to T \in Clsd (J)$
9	7 8	elind	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to T \in (J \cap Clsd (J))$
10	2	subg0cl	$⊢ T \in SubGrp (G) \to \underset{˙}{0} \in T$
11	10	3ad2ant2	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to \underset{˙}{0} \in T$
12	4	conncompclo	$⊢ (J \in TopOn (X) \land T \in (J \cap Clsd (J)) \land \underset{˙}{0} \in T) \to S \subseteq T$
13	6 9 11 12	syl3anc	$⊢ (G \in TopGrp \land T \in SubGrp (G) \land T \in J) \to S \subseteq T$

Metamath Proof Explorer