Theorem tgpconncompss

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

	Ref	Expression
Hypotheses	tgpconncomp.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	tgpconncomp.z	⊢ 0 = ( 0g ‘ 𝐺 )
	tgpconncomp.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	tgpconncomp.s	⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
Assertion	tgpconncompss	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		tgpconncomp.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		tgpconncomp.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		tgpconncomp.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
4		tgpconncomp.s	⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
5	3 1	tgptopon	⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6	5	3ad2ant1	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7		simp3	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ 𝐽 )
8	3	opnsubg	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
9	7 8	elind	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
10	2	subg0cl	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑇 )
11	10	3ad2ant2	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 0 ∈ 𝑇 )
12	4	conncompclo	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 0 ∈ 𝑇 ) → 𝑆 ⊆ 𝑇 )
13	6 9 11 12	syl3anc	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ⊆ 𝑇 )