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 
|- X = ( Base ` G )
tgpconncomp.z 
|- .0. = ( 0g ` G )
tgpconncomp.j 
|- J = ( TopOpen ` G )
tgpconncomp.s 
|- S = U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) }
Assertion tgpconncompss 
|- ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> S C_ T )

Proof

Step Hyp Ref Expression
1 tgpconncomp.x 
 |-  X = ( Base ` G )
2 tgpconncomp.z 
 |-  .0. = ( 0g ` G )
3 tgpconncomp.j 
 |-  J = ( TopOpen ` G )
4 tgpconncomp.s 
 |-  S = U. { x e. ~P X | ( .0. e. x /\ ( J |`t x ) e. Conn ) }
5 3 1 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` X ) )
6 5 3ad2ant1 
 |-  ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> J e. ( TopOn ` X ) )
7 simp3 
 |-  ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> T e. J )
8 3 opnsubg 
 |-  ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> T e. ( Clsd ` J ) )
9 7 8 elind 
 |-  ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> T e. ( J i^i ( Clsd ` J ) ) )
10 2 subg0cl 
 |-  ( T e. ( SubGrp ` G ) -> .0. e. T )
11 10 3ad2ant2 
 |-  ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> .0. e. T )
12 4 conncompclo 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ .0. e. T ) -> S C_ T )
13 6 9 11 12 syl3anc 
 |-  ( ( G e. TopGrp /\ T e. ( SubGrp ` G ) /\ T e. J ) -> S C_ T )