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

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 ecelqsw ⊢ ( ( 𝑅 ∈ 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 imbitrdi ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑋 / 𝑅 ) ∈ Fin ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑥 ∈ ( 𝑋 / 𝑅 ) ) → ( ¬ 𝑥 = 𝑆 → 𝑥 ⊆ ( V ∖ 𝑆 ) ) )
50 42 49 biimtrid ⊢ ( ( ( ( 𝐺 ∈ 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 biimtrid ⊢ ( ( ( 𝐺 ∈ 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 ‘ 𝐽 ) ↔ 𝑆 ∈ 𝐽 ) )