This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑆 ⊆ 𝑇 )