Theorem tgpconncompeqg 24027

Description: The connected component containing 𝐴 is the left coset of the identity component containing 𝐴. (Contributed by Mario Carneiro, 17-Sep-2015.)

Hypotheses

Ref	Expression
tgpconncomp.x	⊢ 𝑋 = (Base‘𝐺)
tgpconncomp.z	⊢ 0 = (0g‘𝐺)
tgpconncomp.j	⊢ 𝐽 = (TopOpen‘𝐺)
tgpconncomp.s	⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
tgpconncompeqg.r	⊢ ∼ = (𝐺 ~QG 𝑆)

Assertion

Ref	Expression
tgpconncompeqg	⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})

Distinct variable groups:   𝑥, 0   𝑥,𝐴   𝑥,𝐽   𝑥,𝐺   𝑥,𝑋

Allowed substitution hints:   ∼ (𝑥)   𝑆(𝑥)

Proof of Theorem tgpconncompeqg

Dummy variables 𝑦 𝑧 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfec2 8625	. . . . 5 ⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
2	1	adantl 481	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
3		tgpconncomp.s	. . . . . . . . 9 ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
4		ssrab2 4027	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋
5		sspwuni 5046	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋)
6	4, 5	mpbi 230	. . . . . . . . 9 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋
7	3, 6	eqsstri 3976	. . . . . . . 8 ⊢ 𝑆 ⊆ 𝑋
8	7	a1i 11	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ 𝑋)
9		tgpconncomp.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
10		eqid 2731	. . . . . . . 8 ⊢ (invg‘𝐺) = (invg‘𝐺)
11		eqid 2731	. . . . . . . 8 ⊢ (+g‘𝐺) = (+g‘𝐺)
12		tgpconncompeqg.r	. . . . . . . 8 ⊢ ∼ = (𝐺 ~QG 𝑆)
13	9, 10, 11, 12	eqgval 19089	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆)))
14	8, 13	syldan 591	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆)))
15		simp2 1137	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆) → 𝑧 ∈ 𝑋)
16	14, 15	biimtrdi 253	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 → 𝑧 ∈ 𝑋))
17	16	abssdv 4014	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → {𝑧 ∣ 𝐴 ∼ 𝑧} ⊆ 𝑋)
18	2, 17	eqsstrd 3964	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ 𝑋)
19		simpr 484	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
20		tgpgrp 23993	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
21		tgpconncomp.z	. . . . . . . 8 ⊢ 0 = (0g‘𝐺)
22	9, 11, 21, 10	grplinv 18902	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
23	20, 22	sylan 580	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
24		tgpconncomp.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝐺)
25	24, 9	tgptopon 23997	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
26	25	adantr 480	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
27	20	adantr 480	. . . . . . . 8 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ Grp)
28	9, 21	grpidcl 18878	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋)
29	27, 28	syl 17	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑋)
30	3	conncompid 23346	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆)
31	26, 29, 30	syl2anc 584	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑆)
32	23, 31	eqeltrd 2831	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)
33	9, 10, 11, 12	eqgval 19089	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
34	8, 33	syldan 591	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
35	19, 19, 32, 34	mpbir3and 1343	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∼ 𝐴)
36		elecg 8666	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
37	19, 19, 36	syl2anc 584	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
38	35, 37	mpbird 257	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴] ∼ )
39	9, 12, 11	eqglact 19091	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
40	7, 39	mp3an2 1451	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
41	20, 40	sylan 580	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
42	41	oveq2d 7362	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) = (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
43		eqid 2731	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
44		eqid 2731	. . . . . . 7 ⊢ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))
45	44, 9, 11, 24	tgplacthmeo 24018	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
46		hmeocn 23675	. . . . . 6 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
47	45, 46	syl 17	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
48		toponuni 22829	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
49	26, 48	syl 17	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
50	7, 49	sseqtrid 3972	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽)
51	3	conncompconn 23347	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
52	26, 29, 51	syl2anc 584	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
53	43, 47, 50, 52	connima 23340	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn)
54	42, 53	eqeltrd 2831	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) ∈ Conn)
55		eqid 2731	. . . 4 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
56	55	conncompss 23348	. . 3 ⊢ (([𝐴] ∼ ⊆ 𝑋 ∧ 𝐴 ∈ [𝐴] ∼ ∧ (𝐽 ↾t [𝐴] ∼ ) ∈ Conn) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
57	18, 38, 54, 56	syl3anc 1373	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
58		elpwi 4554	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
59	44	mptpreima 6185	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) = {𝑧 ∈ 𝑋 ∣ (𝐴(+g‘𝐺)𝑧) ∈ 𝑦}
60	59	ssrab3 4029	. . . . . . . . . 10 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋
61	29	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ 𝑋)
62	9, 11, 21	grprid 18881	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
63	20, 62	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
64	63	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
65		simprrl 780	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝐴 ∈ 𝑦)
66	64, 65	eqeltrd 2831	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) ∈ 𝑦)
67		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → (𝐴(+g‘𝐺)𝑧) = (𝐴(+g‘𝐺) 0 ))
68	67	eleq1d 2816	. . . . . . . . . . . 12 ⊢ (𝑧 = 0 → ((𝐴(+g‘𝐺)𝑧) ∈ 𝑦 ↔ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
69	68, 59	elrab2 3645	. . . . . . . . . . 11 ⊢ ( 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ↔ ( 0 ∈ 𝑋 ∧ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
70	61, 66, 69	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦))
71		hmeocnvcn 23676	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
72	45, 71	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
73	72	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
74		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ 𝑋)
75	49	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑋 = ∪ 𝐽)
76	74, 75	sseqtrd 3966	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ ∪ 𝐽)
77		simprrr 781	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t 𝑦) ∈ Conn)
78	43, 73, 76, 77	connima 23340	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn)
79	3	conncompss 23348	. . . . . . . . . 10 ⊢ (((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋 ∧ 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ∧ (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
80	60, 70, 78, 79	mp3an2i 1468	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
81		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧))) = (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))
82	81, 9, 11, 10	grplactcnv 18956	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘((invg‘𝐺)‘𝐴))))
83	20, 82	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘((invg‘𝐺)‘𝐴))))
84	83	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋)
85	81, 9	grplactfval 18954	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
86	85	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
87	86	f1oeq1d 6758	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋))
88	84, 87	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
89	88	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
90		f1ocnv 6775	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
91		f1ofun 6765	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
92	89, 90, 91	3syl 18	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
93		f1odm 6767	. . . . . . . . . . . 12 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
94	89, 90, 93	3syl 18	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
95	74, 94	sseqtrrd 3967	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
96		funimass3 6987	. . . . . . . . . 10 ⊢ ((Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∧ 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
97	92, 95, 96	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
98	80, 97	mpbid 232	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
99	41	adantr 480	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
100		imacnvcnv 6153	. . . . . . . . 9 ⊢ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆) = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)
101	99, 100	eqtr4di 2784	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
102	98, 101	sseqtrrd 3967	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ [𝐴] ∼ )
103	102	expr 456	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ⊆ 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
104	58, 103	sylan2 593	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝒫 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
105	104	ralrimiva 3124	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
106		eleq2w 2815	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
107		oveq2 7354	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐽 ↾t 𝑥) = (𝐽 ↾t 𝑦))
108	107	eleq1d 2816	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝐽 ↾t 𝑥) ∈ Conn ↔ (𝐽 ↾t 𝑦) ∈ Conn))
109	106, 108	anbi12d 632	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn) ↔ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn)))
110	109	ralrab 3648	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
111	105, 110	sylibr 234	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
112		unissb 4889	. . 3 ⊢ (∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
113	111, 112	sylibr 234	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ )
114	57, 113	eqssd 3947	1 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  {cab 2709  ∀wral 3047  {crab 3395   ⊆ wss 3897  𝒫 cpw 4547  ∪ cuni 4856   class class class wbr 5089   ↦ cmpt 5170  ^◡ccnv 5613  dom cdm 5614   “ cima 5617  Fun wfun 6475  –1-1-onto→wf1o 6480  ‘cfv 6481  (class class class)co 7346  [cec 8620  Basecbs 17120  +_gcplusg 17161   ↾_t crest 17324  TopOpenctopn 17325  0_gc0g 17343  Grpcgrp 18846  inv_gcminusg 18847   ~_QG cqg 19035  TopOnctopon 22825   Cn ccn 23139  Conncconn 23326  Homeochmeo 23668  TopGrpctgp 23986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-ec 8624  df-map 8752  df-en 8870  df-fin 8873  df-fi 9295  df-rest 17326  df-0g 17345  df-topgen 17347  df-plusf 18547  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-grp 18849  df-minusg 18850  df-eqg 19038  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22861  df-cld 22934  df-cn 23142  df-cnp 23143  df-conn 23327  df-tx 23477  df-hmeo 23670  df-tmd 23987  df-tgp 23988

This theorem is referenced by:  tgpconncomp  24028