Metamath Proof Explorer


Theorem cldsubg

Description: A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses subgntr.h 𝐽 = ( TopOpen ‘ 𝐺 )
cldsubg.1 𝑅 = ( 𝐺 ~QG 𝑆 )
cldsubg.2 𝑋 = ( Base ‘ 𝐺 )
Assertion cldsubg ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ 𝑆𝐽 ) )

Proof

Step Hyp Ref Expression
1 subgntr.h 𝐽 = ( TopOpen ‘ 𝐺 )
2 cldsubg.1 𝑅 = ( 𝐺 ~QG 𝑆 )
3 cldsubg.2 𝑋 = ( Base ‘ 𝐺 )
4 simpl1 ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐺 ∈ TopGrp )
5 1 3 tgptopon ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 4 5 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
8 6 7 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑋 = 𝐽 )
9 8 difeq1d ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) = ( 𝐽 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) )
10 simpl2 ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
11 unisng ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → { 𝑆 } = 𝑆 )
12 10 11 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → { 𝑆 } = 𝑆 )
13 12 uneq2d ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ 𝑆 ) )
14 uniun ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } )
15 undif1 ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = ( ( 𝑋 / 𝑅 ) ∪ { 𝑆 } )
16 eqid ( 0g𝐺 ) = ( 0g𝐺 )
17 3 2 16 eqgid ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → [ ( 0g𝐺 ) ] 𝑅 = 𝑆 )
18 10 17 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → [ ( 0g𝐺 ) ] 𝑅 = 𝑆 )
19 2 ovexi 𝑅 ∈ V
20 tgpgrp ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
21 4 20 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐺 ∈ Grp )
22 3 16 grpidcl ( 𝐺 ∈ Grp → ( 0g𝐺 ) ∈ 𝑋 )
23 21 22 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 0g𝐺 ) ∈ 𝑋 )
24 ecelqsg ( ( 𝑅 ∈ V ∧ ( 0g𝐺 ) ∈ 𝑋 ) → [ ( 0g𝐺 ) ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
25 19 23 24 sylancr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → [ ( 0g𝐺 ) ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
26 18 25 eqeltrrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑆 ∈ ( 𝑋 / 𝑅 ) )
27 26 snssd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → { 𝑆 } ⊆ ( 𝑋 / 𝑅 ) )
28 ssequn2 ( { 𝑆 } ⊆ ( 𝑋 / 𝑅 ) ↔ ( ( 𝑋 / 𝑅 ) ∪ { 𝑆 } ) = ( 𝑋 / 𝑅 ) )
29 27 28 sylib ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∪ { 𝑆 } ) = ( 𝑋 / 𝑅 ) )
30 15 29 eqtrid ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = ( 𝑋 / 𝑅 ) )
31 30 unieqd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = ( 𝑋 / 𝑅 ) )
32 3 2 eqger ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑅 Er 𝑋 )
33 10 32 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑅 Er 𝑋 )
34 19 a1i ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑅 ∈ V )
35 33 34 uniqs2 ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 / 𝑅 ) = 𝑋 )
36 31 35 eqtrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = 𝑋 )
37 14 36 eqtr3id ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ { 𝑆 } ) = 𝑋 )
38 13 37 eqtr3d ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ 𝑆 ) = 𝑋 )
39 difss ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( 𝑋 / 𝑅 )
40 39 unissi ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( 𝑋 / 𝑅 )
41 40 35 sseqtrid ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ 𝑋 )
42 df-ne ( 𝑥𝑆 ↔ ¬ 𝑥 = 𝑆 )
43 33 adantr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → 𝑅 Er 𝑋 )
44 simpr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → 𝑥 ∈ ( 𝑋 / 𝑅 ) )
45 26 adantr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → 𝑆 ∈ ( 𝑋 / 𝑅 ) )
46 43 44 45 qsdisj ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → ( 𝑥 = 𝑆 ∨ ( 𝑥𝑆 ) = ∅ ) )
47 46 ord ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → ( ¬ 𝑥 = 𝑆 → ( 𝑥𝑆 ) = ∅ ) )
48 disj2 ( ( 𝑥𝑆 ) = ∅ ↔ 𝑥 ⊆ ( V ∖ 𝑆 ) )
49 47 48 syl6ib ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → ( ¬ 𝑥 = 𝑆𝑥 ⊆ ( V ∖ 𝑆 ) ) )
50 42 49 syl5bi ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → ( 𝑥𝑆𝑥 ⊆ ( V ∖ 𝑆 ) ) )
51 50 expimpd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑥 ∈ ( 𝑋 / 𝑅 ) ∧ 𝑥𝑆 ) → 𝑥 ⊆ ( V ∖ 𝑆 ) ) )
52 eldifsn ( 𝑥 ∈ ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ↔ ( 𝑥 ∈ ( 𝑋 / 𝑅 ) ∧ 𝑥𝑆 ) )
53 velpw ( 𝑥 ∈ 𝒫 ( V ∖ 𝑆 ) ↔ 𝑥 ⊆ ( V ∖ 𝑆 ) )
54 51 52 53 3imtr4g ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∈ ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) → 𝑥 ∈ 𝒫 ( V ∖ 𝑆 ) ) )
55 54 ssrdv ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ 𝒫 ( V ∖ 𝑆 ) )
56 sspwuni ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ 𝒫 ( V ∖ 𝑆 ) ↔ ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( V ∖ 𝑆 ) )
57 55 56 sylib ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( V ∖ 𝑆 ) )
58 disj2 ( ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∩ 𝑆 ) = ∅ ↔ ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( V ∖ 𝑆 ) )
59 57 58 sylibr ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∩ 𝑆 ) = ∅ )
60 uneqdifeq ( ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ 𝑋 ∧ ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∩ 𝑆 ) = ∅ ) → ( ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ 𝑆 ) = 𝑋 ↔ ( 𝑋 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) = 𝑆 ) )
61 41 59 60 syl2anc ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∪ 𝑆 ) = 𝑋 ↔ ( 𝑋 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) = 𝑆 ) )
62 38 61 mpbid ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) = 𝑆 )
63 9 62 eqtr3d ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) = 𝑆 )
64 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
65 6 64 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top )
66 simpl3 ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 / 𝑅 ) ∈ Fin )
67 diffi ( ( 𝑋 / 𝑅 ) ∈ Fin → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∈ Fin )
68 66 67 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∈ Fin )
69 vex 𝑥 ∈ V
70 69 elqs ( 𝑥 ∈ ( 𝑋 / 𝑅 ) ↔ ∃ 𝑦𝑋 𝑥 = [ 𝑦 ] 𝑅 )
71 simpll2 ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
72 subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
73 71 72 syl ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → 𝐺 ∈ Grp )
74 3 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆𝑋 )
75 10 74 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑆𝑋 )
76 75 adantr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → 𝑆𝑋 )
77 simpr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → 𝑦𝑋 )
78 eqid ( +g𝐺 ) = ( +g𝐺 )
79 3 2 78 eqglact ( ( 𝐺 ∈ Grp ∧ 𝑆𝑋𝑦𝑋 ) → [ 𝑦 ] 𝑅 = ( ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) “ 𝑆 ) )
80 73 76 77 79 syl3anc ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → [ 𝑦 ] 𝑅 = ( ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) “ 𝑆 ) )
81 simplr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
82 eqid ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) = ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) )
83 82 3 78 1 tgplacthmeo ( ( 𝐺 ∈ TopGrp ∧ 𝑦𝑋 ) → ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
84 4 83 sylan ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
85 75 8 sseqtrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑆 𝐽 )
86 85 adantr ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → 𝑆 𝐽 )
87 eqid 𝐽 = 𝐽
88 87 hmeocld ( ( ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ 𝑆 𝐽 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) “ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ) )
89 84 86 88 syl2anc ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) “ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ) )
90 81 89 mpbid ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → ( ( 𝑧𝑋 ↦ ( 𝑦 ( +g𝐺 ) 𝑧 ) ) “ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
91 80 90 eqeltrd ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → [ 𝑦 ] 𝑅 ∈ ( Clsd ‘ 𝐽 ) )
92 eleq1 ( 𝑥 = [ 𝑦 ] 𝑅 → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ [ 𝑦 ] 𝑅 ∈ ( Clsd ‘ 𝐽 ) ) )
93 91 92 syl5ibrcom ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑦𝑋 ) → ( 𝑥 = [ 𝑦 ] 𝑅𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
94 93 rexlimdva ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∃ 𝑦𝑋 𝑥 = [ 𝑦 ] 𝑅𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
95 70 94 syl5bi ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∈ ( 𝑋 / 𝑅 ) → 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
96 95 ssrdv ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑋 / 𝑅 ) ⊆ ( Clsd ‘ 𝐽 ) )
97 96 ssdifssd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( Clsd ‘ 𝐽 ) )
98 87 unicld ( ( 𝐽 ∈ Top ∧ ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∈ Fin ∧ ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ⊆ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∈ ( Clsd ‘ 𝐽 ) )
99 65 68 97 98 syl3anc ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∈ ( Clsd ‘ 𝐽 ) )
100 87 cldopn ( ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ∈ ( Clsd ‘ 𝐽 ) → ( 𝐽 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) ∈ 𝐽 )
101 99 100 syl ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ( ( 𝑋 / 𝑅 ) ∖ { 𝑆 } ) ) ∈ 𝐽 )
102 63 101 eqeltrrd ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑆𝐽 )
103 102 ex ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆𝐽 ) )
104 1 opnsubg ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆𝐽 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
105 104 3expia ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆𝐽𝑆 ∈ ( Clsd ‘ 𝐽 ) ) )
106 105 3adant3 ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) → ( 𝑆𝐽𝑆 ∈ ( Clsd ‘ 𝐽 ) ) )
107 103 106 impbid ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ 𝑆𝐽 ) )