Step | Hyp | Ref
| Expression |
1 | | simpl1 1248 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐺 ∈ TopGrp) |
2 | | subgntr.h |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝐺) |
3 | | cldsubg.2 |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
4 | 2, 3 | tgptopon 22257 |
. . . . . . . 8
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐽 ∈ (TopOn‘𝑋)) |
6 | | toponuni 21090 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑋 = ∪ 𝐽) |
8 | 7 | difeq1d 3955 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 ∖ ∪
((𝑋 / 𝑅) ∖ {𝑆})) = (∪ 𝐽 ∖ ∪ ((𝑋
/ 𝑅) ∖ {𝑆}))) |
9 | | simpl2 1250 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ∈ (SubGrp‘𝐺)) |
10 | | unisng 4674 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∪ {𝑆}
= 𝑆) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
{𝑆} = 𝑆) |
12 | 11 | uneq2d 3995 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪
((𝑋 / 𝑅) ∖ {𝑆}) ∪ ∪ {𝑆}) = (∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ∪ 𝑆)) |
13 | | uniun 4680 |
. . . . . . . 8
⊢ ∪ (((𝑋
/ 𝑅) ∖ {𝑆}) ∪ {𝑆}) = (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ ∪ {𝑆}) |
14 | | undif1 4267 |
. . . . . . . . . . 11
⊢ (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = ((𝑋 / 𝑅) ∪ {𝑆}) |
15 | | cldsubg.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝑅 = (𝐺 ~QG 𝑆) |
16 | | eqid 2826 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝐺) = (0g‘𝐺) |
17 | 3, 15, 16 | eqgid 17998 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
[(0g‘𝐺)]𝑅 = 𝑆) |
18 | 9, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → [(0g‘𝐺)]𝑅 = 𝑆) |
19 | | ovex 6938 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ~QG 𝑆) ∈ V |
20 | 15, 19 | eqeltri 2903 |
. . . . . . . . . . . . . . 15
⊢ 𝑅 ∈ V |
21 | | tgpgrp 22253 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
22 | 1, 21 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐺 ∈ Grp) |
23 | 3, 16 | grpidcl 17805 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (0g‘𝐺) ∈ 𝑋) |
25 | | ecelqsg 8068 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ V ∧
(0g‘𝐺)
∈ 𝑋) →
[(0g‘𝐺)]𝑅 ∈ (𝑋 / 𝑅)) |
26 | 20, 24, 25 | sylancr 583 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → [(0g‘𝐺)]𝑅 ∈ (𝑋 / 𝑅)) |
27 | 18, 26 | eqeltrrd 2908 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ∈ (𝑋 / 𝑅)) |
28 | 27 | snssd 4559 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → {𝑆} ⊆ (𝑋 / 𝑅)) |
29 | | ssequn2 4014 |
. . . . . . . . . . . 12
⊢ ({𝑆} ⊆ (𝑋 / 𝑅) ↔ ((𝑋 / 𝑅) ∪ {𝑆}) = (𝑋 / 𝑅)) |
30 | 28, 29 | sylib 210 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∪ {𝑆}) = (𝑋 / 𝑅)) |
31 | 14, 30 | syl5eq 2874 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = (𝑋 / 𝑅)) |
32 | 31 | unieqd 4669 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
(((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = ∪ (𝑋 / 𝑅)) |
33 | 3, 15 | eqger 17996 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑅 Er 𝑋) |
34 | 9, 33 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑅 Er 𝑋) |
35 | 20 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑅 ∈ V) |
36 | 34, 35 | uniqs2 8075 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
(𝑋 / 𝑅) = 𝑋) |
37 | 32, 36 | eqtrd 2862 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
(((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = 𝑋) |
38 | 13, 37 | syl5eqr 2876 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪
((𝑋 / 𝑅) ∖ {𝑆}) ∪ ∪ {𝑆}) = 𝑋) |
39 | 12, 38 | eqtr3d 2864 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪
((𝑋 / 𝑅) ∖ {𝑆}) ∪ 𝑆) = 𝑋) |
40 | | difss 3965 |
. . . . . . . . 9
⊢ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (𝑋 / 𝑅) |
41 | 40 | unissi 4684 |
. . . . . . . 8
⊢ ∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ⊆ ∪ (𝑋
/ 𝑅) |
42 | 41, 36 | syl5sseq 3879 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝑋) |
43 | | df-ne 3001 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≠ 𝑆 ↔ ¬ 𝑥 = 𝑆) |
44 | 34 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → 𝑅 Er 𝑋) |
45 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → 𝑥 ∈ (𝑋 / 𝑅)) |
46 | 27 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → 𝑆 ∈ (𝑋 / 𝑅)) |
47 | 44, 45, 46 | qsdisj 8090 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (𝑥 = 𝑆 ∨ (𝑥 ∩ 𝑆) = ∅)) |
48 | 47 | ord 897 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (¬ 𝑥 = 𝑆 → (𝑥 ∩ 𝑆) = ∅)) |
49 | | disj2 4250 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ 𝑆) = ∅ ↔ 𝑥 ⊆ (V ∖ 𝑆)) |
50 | 48, 49 | syl6ib 243 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (¬ 𝑥 = 𝑆 → 𝑥 ⊆ (V ∖ 𝑆))) |
51 | 43, 50 | syl5bi 234 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (𝑥 ≠ 𝑆 → 𝑥 ⊆ (V ∖ 𝑆))) |
52 | 51 | expimpd 447 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑥 ∈ (𝑋 / 𝑅) ∧ 𝑥 ≠ 𝑆) → 𝑥 ⊆ (V ∖ 𝑆))) |
53 | | eldifsn 4537 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑋 / 𝑅) ∖ {𝑆}) ↔ (𝑥 ∈ (𝑋 / 𝑅) ∧ 𝑥 ≠ 𝑆)) |
54 | | selpw 4386 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 (V ∖
𝑆) ↔ 𝑥 ⊆ (V ∖ 𝑆)) |
55 | 52, 53, 54 | 3imtr4g 288 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝑋 / 𝑅) ∖ {𝑆}) → 𝑥 ∈ 𝒫 (V ∖ 𝑆))) |
56 | 55 | ssrdv 3834 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝒫 (V ∖ 𝑆)) |
57 | | sspwuni 4833 |
. . . . . . . . 9
⊢ (((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝒫 (V ∖ 𝑆) ↔ ∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ⊆ (V ∖ 𝑆)) |
58 | 56, 57 | sylib 210 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (V ∖ 𝑆)) |
59 | | disj2 4250 |
. . . . . . . 8
⊢ ((∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ∩ 𝑆) = ∅ ↔ ∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ⊆ (V ∖ 𝑆)) |
60 | 58, 59 | sylibr 226 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪
((𝑋 / 𝑅) ∖ {𝑆}) ∩ 𝑆) = ∅) |
61 | | uneqdifeq 4281 |
. . . . . . 7
⊢ ((∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ⊆ 𝑋 ∧ (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∩ 𝑆) = ∅) → ((∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ∪ 𝑆) = 𝑋 ↔ (𝑋 ∖ ∪
((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆)) |
62 | 42, 60, 61 | syl2anc 581 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((∪
((𝑋 / 𝑅) ∖ {𝑆}) ∪ 𝑆) = 𝑋 ↔ (𝑋 ∖ ∪
((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆)) |
63 | 39, 62 | mpbid 224 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 ∖ ∪
((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆) |
64 | 8, 63 | eqtr3d 2864 |
. . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪
𝐽 ∖ ∪ ((𝑋
/ 𝑅) ∖ {𝑆})) = 𝑆) |
65 | | topontop 21089 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
66 | 5, 65 | syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top) |
67 | | simpl3 1252 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 / 𝑅) ∈ Fin) |
68 | | diffi 8462 |
. . . . . . 7
⊢ ((𝑋 / 𝑅) ∈ Fin → ((𝑋 / 𝑅) ∖ {𝑆}) ∈ Fin) |
69 | 67, 68 | syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∖ {𝑆}) ∈ Fin) |
70 | | vex 3418 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
71 | 70 | elqs 8065 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑋 / 𝑅) ↔ ∃𝑦 ∈ 𝑋 𝑥 = [𝑦]𝑅) |
72 | | simpll2 1277 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈ (SubGrp‘𝐺)) |
73 | | subgrcl 17951 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝐺 ∈ Grp) |
75 | 3 | subgss 17947 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑋) |
76 | 9, 75 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ 𝑋) |
77 | 76 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
78 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
79 | | eqid 2826 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐺) = (+g‘𝐺) |
80 | 3, 15, 79 | eqglact 17997 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑋) → [𝑦]𝑅 = ((𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) “ 𝑆)) |
81 | 74, 77, 78, 80 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → [𝑦]𝑅 = ((𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) “ 𝑆)) |
82 | | simplr 787 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽)) |
83 | | eqid 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) |
84 | 83, 3, 79, 2 | tgplacthmeo 22278 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
85 | 1, 84 | sylan 577 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
86 | 76, 7 | sseqtrd 3867 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ ∪ 𝐽) |
87 | 86 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽) |
88 | | eqid 2826 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝐽 =
∪ 𝐽 |
89 | 88 | hmeocld 21942 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) ∧ 𝑆 ⊆ ∪ 𝐽) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) “ 𝑆) ∈ (Clsd‘𝐽))) |
90 | 85, 87, 89 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) “ 𝑆) ∈ (Clsd‘𝐽))) |
91 | 82, 90 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑦(+g‘𝐺)𝑧)) “ 𝑆) ∈ (Clsd‘𝐽)) |
92 | 81, 91 | eqeltrd 2907 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → [𝑦]𝑅 ∈ (Clsd‘𝐽)) |
93 | | eleq1 2895 |
. . . . . . . . . . 11
⊢ (𝑥 = [𝑦]𝑅 → (𝑥 ∈ (Clsd‘𝐽) ↔ [𝑦]𝑅 ∈ (Clsd‘𝐽))) |
94 | 92, 93 | syl5ibrcom 239 |
. . . . . . . . . 10
⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → (𝑥 = [𝑦]𝑅 → 𝑥 ∈ (Clsd‘𝐽))) |
95 | 94 | rexlimdva 3241 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∃𝑦 ∈ 𝑋 𝑥 = [𝑦]𝑅 → 𝑥 ∈ (Clsd‘𝐽))) |
96 | 71, 95 | syl5bi 234 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑥 ∈ (𝑋 / 𝑅) → 𝑥 ∈ (Clsd‘𝐽))) |
97 | 96 | ssrdv 3834 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 / 𝑅) ⊆ (Clsd‘𝐽)) |
98 | 97 | ssdifssd 3976 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (Clsd‘𝐽)) |
99 | 88 | unicld 21222 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ ((𝑋 / 𝑅) ∖ {𝑆}) ∈ Fin ∧ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (Clsd‘𝐽)) → ∪
((𝑋 / 𝑅) ∖ {𝑆}) ∈ (Clsd‘𝐽)) |
100 | 66, 69, 98, 99 | syl3anc 1496 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪
((𝑋 / 𝑅) ∖ {𝑆}) ∈ (Clsd‘𝐽)) |
101 | 88 | cldopn 21207 |
. . . . 5
⊢ (∪ ((𝑋
/ 𝑅) ∖ {𝑆}) ∈ (Clsd‘𝐽) → (∪ 𝐽
∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) ∈ 𝐽) |
102 | 100, 101 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪
𝐽 ∖ ∪ ((𝑋
/ 𝑅) ∖ {𝑆})) ∈ 𝐽) |
103 | 64, 102 | eqeltrrd 2908 |
. . 3
⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ∈ 𝐽) |
104 | 103 | ex 403 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ∈ 𝐽)) |
105 | 2 | opnsubg 22282 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽)) |
106 | 105 | 3expia 1156 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 ∈ 𝐽 → 𝑆 ∈ (Clsd‘𝐽))) |
107 | 106 | 3adant3 1168 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ 𝐽 → 𝑆 ∈ (Clsd‘𝐽))) |
108 | 104, 107 | impbid 204 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ (Clsd‘𝐽) ↔ 𝑆 ∈ 𝐽)) |