Theorem tgpconncompeqg 24032

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 8651	. . . . 5 ⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
2	1	adantl 481	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
3		tgpconncomp.s	. . . . . . . . 9 ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
4		ssrab2 4039	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋
5		sspwuni 5059	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋)
6	4, 5	mpbi 230	. . . . . . . . 9 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋
7	3, 6	eqsstri 3990	. . . . . . . 8 ⊢ 𝑆 ⊆ 𝑋
8	7	a1i 11	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ 𝑋)
9		tgpconncomp.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
10		eqid 2729	. . . . . . . 8 ⊢ (invg‘𝐺) = (invg‘𝐺)
11		eqid 2729	. . . . . . . 8 ⊢ (+g‘𝐺) = (+g‘𝐺)
12		tgpconncompeqg.r	. . . . . . . 8 ⊢ ∼ = (𝐺 ~QG 𝑆)
13	9, 10, 11, 12	eqgval 19091	. . . . . . 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 4028	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → {𝑧 ∣ 𝐴 ∼ 𝑧} ⊆ 𝑋)
18	2, 17	eqsstrd 3978	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ 𝑋)
19		simpr 484	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
20		tgpgrp 23998	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
21		tgpconncomp.z	. . . . . . . 8 ⊢ 0 = (0g‘𝐺)
22	9, 11, 21, 10	grplinv 18903	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
23	20, 22	sylan 580	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
24		tgpconncomp.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝐺)
25	24, 9	tgptopon 24002	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
26	25	adantr 480	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
27	20	adantr 480	. . . . . . . 8 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ Grp)
28	9, 21	grpidcl 18879	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋)
29	27, 28	syl 17	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑋)
30	3	conncompid 23351	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆)
31	26, 29, 30	syl2anc 584	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑆)
32	23, 31	eqeltrd 2828	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)
33	9, 10, 11, 12	eqgval 19091	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
34	8, 33	syldan 591	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
35	19, 19, 32, 34	mpbir3and 1343	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∼ 𝐴)
36		elecg 8692	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
37	19, 19, 36	syl2anc 584	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
38	35, 37	mpbird 257	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴] ∼ )
39	9, 12, 11	eqglact 19093	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
40	7, 39	mp3an2 1451	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
41	20, 40	sylan 580	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
42	41	oveq2d 7385	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) = (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
43		eqid 2729	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
44		eqid 2729	. . . . . . 7 ⊢ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))
45	44, 9, 11, 24	tgplacthmeo 24023	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
46		hmeocn 23680	. . . . . 6 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
47	45, 46	syl 17	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
48		toponuni 22834	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
49	26, 48	syl 17	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
50	7, 49	sseqtrid 3986	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽)
51	3	conncompconn 23352	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
52	26, 29, 51	syl2anc 584	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
53	43, 47, 50, 52	connima 23345	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn)
54	42, 53	eqeltrd 2828	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) ∈ Conn)
55		eqid 2729	. . . 4 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
56	55	conncompss 23353	. . 3 ⊢ (([𝐴] ∼ ⊆ 𝑋 ∧ 𝐴 ∈ [𝐴] ∼ ∧ (𝐽 ↾t [𝐴] ∼ ) ∈ Conn) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
57	18, 38, 54, 56	syl3anc 1373	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
58		elpwi 4566	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
59	44	mptpreima 6199	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) = {𝑧 ∈ 𝑋 ∣ (𝐴(+g‘𝐺)𝑧) ∈ 𝑦}
60	59	ssrab3 4041	. . . . . . . . . 10 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋
61	29	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ 𝑋)
62	9, 11, 21	grprid 18882	. . . . . . . . . . . . . 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 2828	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) ∈ 𝑦)
67		oveq2 7377	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → (𝐴(+g‘𝐺)𝑧) = (𝐴(+g‘𝐺) 0 ))
68	67	eleq1d 2813	. . . . . . . . . . . 12 ⊢ (𝑧 = 0 → ((𝐴(+g‘𝐺)𝑧) ∈ 𝑦 ↔ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
69	68, 59	elrab2 3659	. . . . . . . . . . 11 ⊢ ( 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ↔ ( 0 ∈ 𝑋 ∧ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
70	61, 66, 69	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦))
71		hmeocnvcn 23681	. . . . . . . . . . . . 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 3980	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ ∪ 𝐽)
77		simprrr 781	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t 𝑦) ∈ Conn)
78	43, 73, 76, 77	connima 23345	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn)
79	3	conncompss 23353	. . . . . . . . . 10 ⊢ (((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋 ∧ 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ∧ (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
80	60, 70, 78, 79	mp3an2i 1468	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
81		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧))) = (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))
82	81, 9, 11, 10	grplactcnv 18957	. . . . . . . . . . . . . . 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 18955	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
86	85	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
87	86	f1oeq1d 6777	. . . . . . . . . . . . 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 6794	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
91		f1ofun 6784	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
92	89, 90, 91	3syl 18	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
93		f1odm 6786	. . . . . . . . . . . 12 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
94	89, 90, 93	3syl 18	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
95	74, 94	sseqtrrd 3981	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
96		funimass3 7008	. . . . . . . . . 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 6167	. . . . . . . . 9 ⊢ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆) = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)
101	99, 100	eqtr4di 2782	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
102	98, 101	sseqtrrd 3981	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ [𝐴] ∼ )
103	102	expr 456	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ⊆ 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
104	58, 103	sylan2 593	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝒫 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
105	104	ralrimiva 3125	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
106		eleq2w 2812	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
107		oveq2 7377	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐽 ↾t 𝑥) = (𝐽 ↾t 𝑦))
108	107	eleq1d 2813	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝐽 ↾t 𝑥) ∈ Conn ↔ (𝐽 ↾t 𝑦) ∈ Conn))
109	106, 108	anbi12d 632	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn) ↔ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn)))
110	109	ralrab 3662	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
111	105, 110	sylibr 234	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
112		unissb 4899	. . 3 ⊢ (∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
113	111, 112	sylibr 234	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ )
114	57, 113	eqssd 3961	1 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  {crab 3402   ⊆ wss 3911  𝒫 cpw 4559  ∪ cuni 4867   class class class wbr 5102   ↦ cmpt 5183  ^◡ccnv 5630  dom cdm 5631   “ cima 5634  Fun wfun 6493  –1-1-onto→wf1o 6498  ‘cfv 6499  (class class class)co 7369  [cec 8646  Basecbs 17155  +_gcplusg 17196   ↾_t crest 17359  TopOpenctopn 17360  0_gc0g 17378  Grpcgrp 18847  inv_gcminusg 18848   ~_QG cqg 19036  TopOnctopon 22830   Cn ccn 23144  Conncconn 23331  Homeochmeo 23673  TopGrpctgp 23991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-ec 8650  df-map 8778  df-en 8896  df-fin 8899  df-fi 9338  df-rest 17361  df-0g 17380  df-topgen 17382  df-plusf 18548  df-mgm 18549  df-sgrp 18628  df-mnd 18644  df-grp 18850  df-minusg 18851  df-eqg 19039  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22866  df-cld 22939  df-cn 23147  df-cnp 23148  df-conn 23332  df-tx 23482  df-hmeo 23675  df-tmd 23992  df-tgp 23993

This theorem is referenced by:  tgpconncomp  24033