| 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 ‘ 𝐽 ) ↔ 𝑆 ∈ 𝐽 ) ) |