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
|
syl5eq |
⊢ ( ( ( 𝐺 ∈ 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 ‘ 𝐽 ) ↔ 𝑆 ∈ 𝐽 ) ) |