Theorem tgpconncompeqg 23272

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 8510	. . . . 5 ⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
2	1	adantl 482	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧})
3		tgpconncomp.s	. . . . . . . . 9 ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
4		ssrab2 4014	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋
5		sspwuni 5030	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋)
6	4, 5	mpbi 229	. . . . . . . . 9 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ 𝑋
7	3, 6	eqsstri 3956	. . . . . . . 8 ⊢ 𝑆 ⊆ 𝑋
8	7	a1i 11	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ 𝑋)
9		tgpconncomp.x	. . . . . . . 8 ⊢ 𝑋 = (Base‘𝐺)
10		eqid 2739	. . . . . . . 8 ⊢ (invg‘𝐺) = (invg‘𝐺)
11		eqid 2739	. . . . . . . 8 ⊢ (+g‘𝐺) = (+g‘𝐺)
12		tgpconncompeqg.r	. . . . . . . 8 ⊢ ∼ = (𝐺 ~QG 𝑆)
13	9, 10, 11, 12	eqgval 18814	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆)))
14	8, 13	syldan 591	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆)))
15		simp2 1136	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆) → 𝑧 ∈ 𝑋)
16	14, 15	syl6bi 252	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 → 𝑧 ∈ 𝑋))
17	16	abssdv 4003	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → {𝑧 ∣ 𝐴 ∼ 𝑧} ⊆ 𝑋)
18	2, 17	eqsstrd 3960	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ 𝑋)
19		simpr 485	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋)
20		tgpgrp 23238	. . . . . . 7 ⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
21		tgpconncomp.z	. . . . . . . 8 ⊢ 0 = (0g‘𝐺)
22	9, 11, 21, 10	grplinv 18637	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
23	20, 22	sylan 580	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 )
24		tgpconncomp.j	. . . . . . . . 9 ⊢ 𝐽 = (TopOpen‘𝐺)
25	24, 9	tgptopon 23242	. . . . . . . 8 ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
26	25	adantr 481	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋))
27	20	adantr 481	. . . . . . . 8 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ Grp)
28	9, 21	grpidcl 18616	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋)
29	27, 28	syl 17	. . . . . . 7 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑋)
30	3	conncompid 22591	. . . . . . 7 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆)
31	26, 29, 30	syl2anc 584	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑆)
32	23, 31	eqeltrd 2840	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)
33	9, 10, 11, 12	eqgval 18814	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
34	8, 33	syldan 591	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆)))
35	19, 19, 32, 34	mpbir3and 1341	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∼ 𝐴)
36		elecg 8550	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
37	19, 19, 36	syl2anc 584	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴))
38	35, 37	mpbird 256	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴] ∼ )
39	9, 12, 11	eqglact 18816	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
40	7, 39	mp3an2 1448	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
41	20, 40	sylan 580	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
42	41	oveq2d 7300	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) = (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
43		eqid 2739	. . . . 5 ⊢ ∪ 𝐽 = ∪ 𝐽
44		eqid 2739	. . . . . . 7 ⊢ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))
45	44, 9, 11, 24	tgplacthmeo 23263	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
46		hmeocn 22920	. . . . . 6 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
47	45, 46	syl 17	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
48		toponuni 22072	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
49	26, 48	syl 17	. . . . . 6 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽)
50	7, 49	sseqtrid 3974	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽)
51	3	conncompconn 22592	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
52	26, 29, 51	syl2anc 584	. . . . 5 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
53	43, 47, 50, 52	connima 22585	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) ∈ Conn)
54	42, 53	eqeltrd 2840	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) ∈ Conn)
55		eqid 2739	. . . 4 ⊢ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}
56	55	conncompss 22593	. . 3 ⊢ (([𝐴] ∼ ⊆ 𝑋 ∧ 𝐴 ∈ [𝐴] ∼ ∧ (𝐽 ↾t [𝐴] ∼ ) ∈ Conn) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
57	18, 38, 54, 56	syl3anc 1370	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})
58		elpwi 4543	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋)
59	44	mptpreima 6146	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) = {𝑧 ∈ 𝑋 ∣ (𝐴(+g‘𝐺)𝑧) ∈ 𝑦}
60	59	ssrab3 4016	. . . . . . . . . 10 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋
61	29	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ 𝑋)
62	9, 11, 21	grprid 18619	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
63	20, 62	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
64	63	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) = 𝐴)
65		simprrl 778	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝐴 ∈ 𝑦)
66	64, 65	eqeltrd 2840	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐴(+g‘𝐺) 0 ) ∈ 𝑦)
67		oveq2 7292	. . . . . . . . . . . . 13 ⊢ (𝑧 = 0 → (𝐴(+g‘𝐺)𝑧) = (𝐴(+g‘𝐺) 0 ))
68	67	eleq1d 2824	. . . . . . . . . . . 12 ⊢ (𝑧 = 0 → ((𝐴(+g‘𝐺)𝑧) ∈ 𝑦 ↔ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
69	68, 59	elrab2 3628	. . . . . . . . . . 11 ⊢ ( 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ↔ ( 0 ∈ 𝑋 ∧ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦))
70	61, 66, 69	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦))
71		hmeocnvcn 22921	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
72	45, 71	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
73	72	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
74		simprl 768	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ 𝑋)
75	49	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑋 = ∪ 𝐽)
76	74, 75	sseqtrd 3962	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ ∪ 𝐽)
77		simprrr 779	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t 𝑦) ∈ Conn)
78	43, 73, 76, 77	connima 22585	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn)
79	3	conncompss 22593	. . . . . . . . . 10 ⊢ (((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋 ∧ 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ∧ (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Conn) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
80	60, 70, 78, 79	mp3an2i 1465	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
81		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧))) = (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))
82	81, 9, 11, 10	grplactcnv 18687	. . . . . . . . . . . . . . 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 495	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋)
85	81, 9	grplactfval 18685	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
86	85	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
87	86	f1oeq1d 6720	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋))
88	84, 87	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
89	88	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
90		f1ocnv 6737	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)
91		f1ofun 6727	. . . . . . . . . . 11 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
92	89, 90, 91	3syl 18	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
93		f1odm 6729	. . . . . . . . . . . 12 ⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
94	89, 90, 93	3syl 18	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋)
95	74, 94	sseqtrrd 3963	. . . . . . . . . 10 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)))
96		funimass3 6940	. . . . . . . . . 10 ⊢ ((Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∧ 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
97	92, 95, 96	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)))
98	80, 97	mpbid 231	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
99	41	adantr 481	. . . . . . . . 9 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
100		imacnvcnv 6114	. . . . . . . . 9 ⊢ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆) = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)
101	99, 100	eqtr4di 2797	. . . . . . . 8 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → [𝐴] ∼ = (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))
102	98, 101	sseqtrrd 3963	. . . . . . 7 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn))) → 𝑦 ⊆ [𝐴] ∼ )
103	102	expr 457	. . . . . 6 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ⊆ 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
104	58, 103	sylan2 593	. . . . 5 ⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝒫 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
105	104	ralrimiva 3104	. . . 4 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
106		eleq2w 2823	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
107		oveq2 7292	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐽 ↾t 𝑥) = (𝐽 ↾t 𝑦))
108	107	eleq1d 2824	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝐽 ↾t 𝑥) ∈ Conn ↔ (𝐽 ↾t 𝑦) ∈ Conn))
109	106, 108	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn) ↔ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn)))
110	109	ralrab 3631	. . . 4 ⊢ (∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ∼ ))
111	105, 110	sylibr 233	. . 3 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
112		unissb 4874	. . 3 ⊢ (∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ ↔ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ∼ )
113	111, 112	sylibr 233	. 2 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⊆ [𝐴] ∼ )
114	57, 113	eqssd 3939	1 ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {cab 2716  ∀wral 3065  {crab 3069   ⊆ wss 3888  𝒫 cpw 4534  ∪ cuni 4840   class class class wbr 5075   ↦ cmpt 5158  ^◡ccnv 5589  dom cdm 5590   “ cima 5593  Fun wfun 6431  –1-1-onto→wf1o 6436  ‘cfv 6437  (class class class)co 7284  [cec 8505  Basecbs 16921  +_gcplusg 16971   ↾_t crest 17140  TopOpenctopn 17141  0_gc0g 17159  Grpcgrp 18586  inv_gcminusg 18587   ~_QG cqg 18760  TopOnctopon 22068   Cn ccn 22384  Conncconn 22571  Homeochmeo 22913  TopGrpctgp 23231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-ec 8509  df-map 8626  df-en 8743  df-fin 8746  df-fi 9179  df-rest 17142  df-0g 17161  df-topgen 17163  df-plusf 18334  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-grp 18589  df-minusg 18590  df-eqg 18763  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-cld 22179  df-cn 22387  df-cnp 22388  df-conn 22572  df-tx 22722  df-hmeo 22915  df-tmd 23232  df-tgp 23233

This theorem is referenced by:  tgpconncomp  23273