Metamath Proof Explorer

Theorem opnsubg

Description: An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis subgntr.h ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion opnsubg ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 subgntr.h ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 2 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
4 3 3ad2ant2 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
5 1 2 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
7 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
8 6 7 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( Base ‘ 𝐺 ) = ∪ 𝐽 )
9 4 8 sseqtrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
10 8 difeq1d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) = ( ∪ 𝐽 ∖ 𝑆 ) )
11 df-ima ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) “ 𝑆 ) = ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ↾ 𝑆 )
12 4 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 12 resmptd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ↾ 𝑆 ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
14 13 rneqd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ran ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ↾ 𝑆 ) = ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
15 11 14 eqtrid ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) “ 𝑆 ) = ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
16 simpl1 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝐺 ∈ TopGrp )
17 eldifi ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
18 17 adantl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
19 eqid ⊢ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
20 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
21 19 2 20 1 tgplacthmeo ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
22 16 18 21 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
23 simpl3 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝑆 ∈ 𝐽 )
24 hmeoima ⊢ ( ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) “ 𝑆 ) ∈ 𝐽 )
25 22 23 24 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( ( 𝑦 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) “ 𝑆 ) ∈ 𝐽 )
26 15 25 eqeltrrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ 𝐽 )
27 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
28 16 27 syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝐺 ∈ Grp )
29 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
30 2 20 29 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
31 28 18 30 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
32 simpl2 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
33 29 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
34 32 33 syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
35 ovex ⊢ ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ V
36 eqid ⊢ ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
37 oveq2 ⊢ ( 𝑦 = ( 0g ‘ 𝐺 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
38 36 37 elrnmpt1s ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ V ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
39 34 35 38 sylancl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
40 31 39 eqeltrrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → 𝑥 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
41 28 adantr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝐺 ∈ Grp )
42 18 adantr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
43 12 sselda ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
44 2 20 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
45 41 42 43 44 syl3anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
46 eldifn ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) → ¬ 𝑥 ∈ 𝑆 )
47 46 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ¬ 𝑥 ∈ 𝑆 )
48 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
49 48 subgsubcl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
50 49 3com23 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ∈ 𝑆 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
51 50 3expia ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
52 32 51 sylan ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
53 2 20 48 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) = 𝑥 )
54 41 42 43 53 syl3anc ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) = 𝑥 )
55 54 eleq1d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ↔ 𝑥 ∈ 𝑆 ) )
56 52 55 sylibd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 → 𝑥 ∈ 𝑆 ) )
57 47 56 mtod ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ¬ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
58 45 57 eldifd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) )
59 58 fmpttd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : 𝑆 ⟶ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) )
60 59 frnd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) )
61 eleq2 ⊢ ( 𝑢 = ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ) )
62 sseq1 ⊢ ( 𝑢 = ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) → ( 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ↔ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) )
63 61 62 anbi12d ⊢ ( 𝑢 = ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) → ( ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ↔ ( 𝑥 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∧ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ) )
64 63 rspcev ⊢ ( ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ 𝐽 ∧ ( 𝑥 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∧ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) )
65 26 40 60 64 syl12anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) )
66 65 ralrimiva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ∀ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) )
67 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
68 6 67 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝐽 ∈ Top )
69 eltop2 ⊢ ( 𝐽 ∈ Top → ( ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ) )
70 68 69 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ) ) )
71 66 70 mpbird ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ( Base ‘ 𝐺 ) ∖ 𝑆 ) ∈ 𝐽 )
72 10 71 eqeltrrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑆 ) ∈ 𝐽 )
73 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
74 73 iscld ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ ∪ 𝐽 ∧ ( ∪ 𝐽 ∖ 𝑆 ) ∈ 𝐽 ) ) )
75 68 74 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ ∪ 𝐽 ∧ ( ∪ 𝐽 ∖ 𝑆 ) ∈ 𝐽 ) ) )
76 9 72 75 mpbir2and ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )