cldsubg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cldsubg		Structured version Visualization version GIF version

Theorem cldsubg 21914

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

**Hypotheses**
Ref	Expression
subgntr.h	⊢ 𝐽 = (TopOpen‘𝐺)
cldsubg.1	⊢ 𝑅 = (𝐺 ~_QG 𝑆)
cldsubg.2	⊢ 𝑋 = (Base‘𝐺)

**Assertion**
Ref	Expression
cldsubg	⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ (Clsd‘𝐽) ↔ 𝑆 ∈ 𝐽))

Proof of Theorem cldsubg Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1064	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐺 ∈ TopGrp)
2		subgntr.h	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝐺)
3		cldsubg.2	. . . . . . . . 9 ⊢ 𝑋 = (Base‘𝐺)
4	2, 3	tgptopon 21886	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
5	1, 4	syl 17	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐽 ∈ (TopOn‘𝑋))
6		toponuni 20719	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
7	5, 6	syl 17	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑋 = ∪ 𝐽)
8	7	difeq1d 3727	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) = (∪ 𝐽 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})))
9		simpl2 1065	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ∈ (SubGrp‘𝐺))
10		unisng 4452	. . . . . . . . 9 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∪ {𝑆} = 𝑆)
11	9, 10	syl 17	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ {𝑆} = 𝑆)
12	11	uneq2d 3767	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ ∪ {𝑆}) = (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ 𝑆))
13		uniun 4456	. . . . . . . 8 ⊢ ∪ (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ ∪ {𝑆})
14		undif1 4043	. . . . . . . . . . 11 ⊢ (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = ((𝑋 / 𝑅) ∪ {𝑆})
15		cldsubg.1	. . . . . . . . . . . . . . . 16 ⊢ 𝑅 = (𝐺 ~_QG 𝑆)
16		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
17	3, 15, 16	eqgid 17646	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → [(0_g‘𝐺)]𝑅 = 𝑆)
18	9, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → [(0_g‘𝐺)]𝑅 = 𝑆)
19		ovex 6678	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ~_QG 𝑆) ∈ V
20	15, 19	eqeltri 2697	. . . . . . . . . . . . . . 15 ⊢ 𝑅 ∈ V
21		tgpgrp 21882	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
22	1, 21	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐺 ∈ Grp)
23	3, 16	grpidcl 17450	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Grp → (0_g‘𝐺) ∈ 𝑋)
24	22, 23	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (0_g‘𝐺) ∈ 𝑋)
25		ecelqsg 7802	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ V ∧ (0_g‘𝐺) ∈ 𝑋) → [(0_g‘𝐺)]𝑅 ∈ (𝑋 / 𝑅))
26	20, 24, 25	sylancr 695	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → [(0_g‘𝐺)]𝑅 ∈ (𝑋 / 𝑅))
27	18, 26	eqeltrrd 2702	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ∈ (𝑋 / 𝑅))
28	27	snssd 4340	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → {𝑆} ⊆ (𝑋 / 𝑅))
29		ssequn2 3786	. . . . . . . . . . . 12 ⊢ ({𝑆} ⊆ (𝑋 / 𝑅) ↔ ((𝑋 / 𝑅) ∪ {𝑆}) = (𝑋 / 𝑅))
30	28, 29	sylib 208	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∪ {𝑆}) = (𝑋 / 𝑅))
31	14, 30	syl5eq 2668	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = (𝑋 / 𝑅))
32	31	unieqd 4446	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = ∪ (𝑋 / 𝑅))
33	3, 15	eqger 17644	. . . . . . . . . . 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 7809	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ (𝑋 / 𝑅) = 𝑋)
37	32, 36	eqtrd 2656	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ (((𝑋 / 𝑅) ∖ {𝑆}) ∪ {𝑆}) = 𝑋)
38	13, 37	syl5eqr 2670	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ ∪ {𝑆}) = 𝑋)
39	12, 38	eqtr3d 2658	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ 𝑆) = 𝑋)
40		difss 3737	. . . . . . . . 9 ⊢ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (𝑋 / 𝑅)
41	40	unissi 4461	. . . . . . . 8 ⊢ ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ ∪ (𝑋 / 𝑅)
42	41, 36	syl5sseq 3653	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝑋)
43		df-ne 2795	. . . . . . . . . . . . 13 ⊢ (𝑥 ≠ 𝑆 ↔ ¬ 𝑥 = 𝑆)
44	34	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → 𝑅 Er 𝑋)
45		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → 𝑥 ∈ (𝑋 / 𝑅))
46	27	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → 𝑆 ∈ (𝑋 / 𝑅))
47	44, 45, 46	qsdisj 7824	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (𝑥 = 𝑆 ∨ (𝑥 ∩ 𝑆) = ∅))
48	47	ord 392	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (¬ 𝑥 = 𝑆 → (𝑥 ∩ 𝑆) = ∅))
49		disj2 4024	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∩ 𝑆) = ∅ ↔ 𝑥 ⊆ (V ∖ 𝑆))
50	48, 49	syl6ib 241	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (¬ 𝑥 = 𝑆 → 𝑥 ⊆ (V ∖ 𝑆)))
51	43, 50	syl5bi 232	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑥 ∈ (𝑋 / 𝑅)) → (𝑥 ≠ 𝑆 → 𝑥 ⊆ (V ∖ 𝑆)))
52	51	expimpd 629	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑥 ∈ (𝑋 / 𝑅) ∧ 𝑥 ≠ 𝑆) → 𝑥 ⊆ (V ∖ 𝑆)))
53		eldifsn 4317	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((𝑋 / 𝑅) ∖ {𝑆}) ↔ (𝑥 ∈ (𝑋 / 𝑅) ∧ 𝑥 ≠ 𝑆))
54		selpw 4165	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 (V ∖ 𝑆) ↔ 𝑥 ⊆ (V ∖ 𝑆))
55	52, 53, 54	3imtr4g 285	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑥 ∈ ((𝑋 / 𝑅) ∖ {𝑆}) → 𝑥 ∈ 𝒫 (V ∖ 𝑆)))
56	55	ssrdv 3609	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝒫 (V ∖ 𝑆))
57		sspwuni 4611	. . . . . . . . 9 ⊢ (((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝒫 (V ∖ 𝑆) ↔ ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (V ∖ 𝑆))
58	56, 57	sylib 208	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (V ∖ 𝑆))
59		disj2 4024	. . . . . . . 8 ⊢ ((∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∩ 𝑆) = ∅ ↔ ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (V ∖ 𝑆))
60	58, 59	sylibr 224	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∩ 𝑆) = ∅)
61		uneqdifeq 4057	. . . . . . 7 ⊢ ((∪ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ 𝑋 ∧ (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∩ 𝑆) = ∅) → ((∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ 𝑆) = 𝑋 ↔ (𝑋 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆))
62	42, 60, 61	syl2anc 693	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∪ 𝑆) = 𝑋 ↔ (𝑋 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆))
63	39, 62	mpbid 222	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆)
64	8, 63	eqtr3d 2658	. . . 4 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) = 𝑆)
65		topontop 20718	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
66	5, 65	syl 17	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top)
67		simpl3 1066	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 / 𝑅) ∈ Fin)
68		diffi 8192	. . . . . . 7 ⊢ ((𝑋 / 𝑅) ∈ Fin → ((𝑋 / 𝑅) ∖ {𝑆}) ∈ Fin)
69	67, 68	syl 17	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∖ {𝑆}) ∈ Fin)
70		vex 3203	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
71	70	elqs 7799	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑋 / 𝑅) ↔ ∃𝑦 ∈ 𝑋 𝑥 = [𝑦]𝑅)
72		simpll2 1101	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈ (SubGrp‘𝐺))
73		subgrcl 17599	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
74	72, 73	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝐺 ∈ Grp)
75	3	subgss 17595	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑋)
76	9, 75	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ 𝑋)
77	76	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ⊆ 𝑋)
78		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
79		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
80	3, 15, 79	eqglact 17645	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑋) → [𝑦]𝑅 = ((𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) “ 𝑆))
81	74, 77, 78, 80	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → [𝑦]𝑅 = ((𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) “ 𝑆))
82		simplr 792	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽))
83		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧))
84	83, 3, 79, 2	tgplacthmeo 21907	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
85	1, 84	sylan 488	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
86	76, 7	sseqtrd 3641	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ⊆ ∪ 𝐽)
87	86	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽)
88		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝐽 = ∪ 𝐽
89	88	hmeocld 21570	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) ∧ 𝑆 ⊆ ∪ 𝐽) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) “ 𝑆) ∈ (Clsd‘𝐽)))
90	85, 87, 89	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) “ 𝑆) ∈ (Clsd‘𝐽)))
91	82, 90	mpbid 222	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝑦(+_g‘𝐺)𝑧)) “ 𝑆) ∈ (Clsd‘𝐽))
92	81, 91	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → [𝑦]𝑅 ∈ (Clsd‘𝐽))
93		eleq1 2689	. . . . . . . . . . 11 ⊢ (𝑥 = [𝑦]𝑅 → (𝑥 ∈ (Clsd‘𝐽) ↔ [𝑦]𝑅 ∈ (Clsd‘𝐽)))
94	92, 93	syl5ibrcom 237	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) ∧ 𝑦 ∈ 𝑋) → (𝑥 = [𝑦]𝑅 → 𝑥 ∈ (Clsd‘𝐽)))
95	94	rexlimdva 3031	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∃𝑦 ∈ 𝑋 𝑥 = [𝑦]𝑅 → 𝑥 ∈ (Clsd‘𝐽)))
96	71, 95	syl5bi 232	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑥 ∈ (𝑋 / 𝑅) → 𝑥 ∈ (Clsd‘𝐽)))
97	96	ssrdv 3609	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝑋 / 𝑅) ⊆ (Clsd‘𝐽))
98	97	ssdifssd 3748	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (Clsd‘𝐽))
99	88	unicld 20850	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ ((𝑋 / 𝑅) ∖ {𝑆}) ∈ Fin ∧ ((𝑋 / 𝑅) ∖ {𝑆}) ⊆ (Clsd‘𝐽)) → ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∈ (Clsd‘𝐽))
100	66, 69, 98, 99	syl3anc 1326	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → ∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∈ (Clsd‘𝐽))
101	88	cldopn 20835	. . . . 5 ⊢ (∪ ((𝑋 / 𝑅) ∖ {𝑆}) ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) ∈ 𝐽)
102	100, 101	syl 17	. . . 4 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ ∪ ((𝑋 / 𝑅) ∖ {𝑆})) ∈ 𝐽)
103	64, 102	eqeltrrd 2702	. . 3 ⊢ (((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) ∧ 𝑆 ∈ (Clsd‘𝐽)) → 𝑆 ∈ 𝐽)
104	103	ex 450	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ∈ 𝐽))
105	2	opnsubg 21911	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽))
106	105	3expia 1267	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 ∈ 𝐽 → 𝑆 ∈ (Clsd‘𝐽)))
107	106	3adant3 1081	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ 𝐽 → 𝑆 ∈ (Clsd‘𝐽)))
108	104, 107	impbid 202	1 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ (Clsd‘𝐽) ↔ 𝑆 ∈ 𝐽))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∃wrex 2913 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 {csn 4177 ∪ cuni 4436 ↦ cmpt 4729 “ cima 5117 ‘cfv 5888 (class class class)co 6650 Er wer 7739 [cec 7740 / cqs 7741 Fincfn 7955 Basecbs 15857 +_gcplusg 15941 TopOpenctopn 16082 0_gc0g 16100 Grpcgrp 17422 SubGrpcsubg 17588 ~_QG cqg 17590 Topctop 20698 TopOnctopon 20715 Clsdccld 20820 Homeochmeo 21556 TopGrpctgp 21875

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-ec 7744 df-qs 7748 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-0g 16102 df-topgen 16104 df-plusf 17241 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-grp 17425 df-minusg 17426 df-sbg 17427 df-subg 17591 df-eqg 17593 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-cn 21031 df-cnp 21032 df-tx 21365 df-hmeo 21558 df-tmd 21876 df-tgp 21877

This theorem is referenced by: (None)

W3C validator