Metamath Proof Explorer

Theorem tgpconncompeqg

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

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

Proof

Step Hyp Ref Expression
1 tgpconncomp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 tgpconncomp.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 tgpconncomp.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
4 tgpconncomp.s ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
5 tgpconncompeqg.r ⊢ ∼ = ( 𝐺 ~QG 𝑆 )
6 dfec2 ⊢ ( 𝐴 ∈ 𝑋 → [ 𝐴 ] ∼ = { 𝑧 ∣ 𝐴 ∼ 𝑧 } )
7 6 adantl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = { 𝑧 ∣ 𝐴 ∼ 𝑧 } )
8 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝒫 𝑋
9 sspwuni ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝒫 𝑋 ↔ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝑋 )
10 8 9 mpbi ⊢ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝑋
11 4 10 eqsstri ⊢ 𝑆 ⊆ 𝑋
12 11 a1i ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
13 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
14 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
15 1 13 14 5 eqgval ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝑧 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) )
16 12 15 syldan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∼ 𝑧 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) ) )
17 simp2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) → 𝑧 ∈ 𝑋 )
18 16 17 syl6bi ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∼ 𝑧 → 𝑧 ∈ 𝑋 ) )
19 18 abssdv ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → { 𝑧 ∣ 𝐴 ∼ 𝑧 } ⊆ 𝑋 )
20 7 19 eqsstrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ ⊆ 𝑋 )
21 simpr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
22 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
23 1 14 2 13 grplinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) = 0 )
24 22 23 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) = 0 )
25 3 1 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
26 25 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
27 22 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐺 ∈ Grp )
28 1 2 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝑋 )
29 27 28 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ∈ 𝑋 )
30 4 conncompid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 0 ∈ 𝑋 ) → 0 ∈ 𝑆 )
31 26 29 30 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ∈ 𝑆 )
32 24 31 eqeltrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 )
33 1 13 14 5 eqgval ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐴 ∼ 𝐴 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 ) ) )
34 12 33 syldan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∼ 𝐴 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ( +g ‘ 𝐺 ) 𝐴 ) ∈ 𝑆 ) ) )
35 21 21 32 34 mpbir3and ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∼ 𝐴 )
36 elecg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝐴 ) )
37 21 21 36 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝐴 ) )
38 35 37 mpbird ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ [ 𝐴 ] ∼ )
39 1 5 14 eqglact ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
40 11 39 mp3an2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
41 22 40 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
42 41 oveq2d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t [ 𝐴 ] ∼ ) = ( 𝐽 ↾t ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ) )
43 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
44 eqid ⊢ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) )
45 44 1 14 3 tgplacthmeo ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
46 hmeocn ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
47 45 46 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
48 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
49 26 48 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 )
50 11 49 sseqtrid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ ∪ 𝐽 )
51 4 conncompconn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 0 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
52 26 29 51 syl2anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
53 43 47 50 52 connima ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ) ∈ Conn )
54 42 53 eqeltrd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t [ 𝐴 ] ∼ ) ∈ Conn )
55 eqid ⊢ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
56 55 conncompss ⊢ ( ( [ 𝐴 ] ∼ ⊆ 𝑋 ∧ 𝐴 ∈ [ 𝐴 ] ∼ ∧ ( 𝐽 ↾t [ 𝐴 ] ∼ ) ∈ Conn ) → [ 𝐴 ] ∼ ⊆ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
57 20 38 54 56 syl3anc ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ ⊆ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
58 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
59 44 mptpreima ⊢ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) = { 𝑧 ∈ 𝑋 ∣ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑦 }
60 59 ssrab3 ⊢ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ⊆ 𝑋
61 29 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 0 ∈ 𝑋 )
62 1 14 2 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +g ‘ 𝐺 ) 0 ) = 𝐴 )
63 22 62 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +g ‘ 𝐺 ) 0 ) = 𝐴 )
64 63 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( 𝐴 ( +g ‘ 𝐺 ) 0 ) = 𝐴 )
65 simprrl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝐴 ∈ 𝑦 )
66 64 65 eqeltrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( 𝐴 ( +g ‘ 𝐺 ) 0 ) ∈ 𝑦 )
67 oveq2 ⊢ ( 𝑧 = 0 → ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝐴 ( +g ‘ 𝐺 ) 0 ) )
68 67 eleq1d ⊢ ( 𝑧 = 0 → ( ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑦 ↔ ( 𝐴 ( +g ‘ 𝐺 ) 0 ) ∈ 𝑦 ) )
69 68 59 elrab2 ⊢ ( 0 ∈ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ↔ ( 0 ∈ 𝑋 ∧ ( 𝐴 ( +g ‘ 𝐺 ) 0 ) ∈ 𝑦 ) )
70 61 66 69 sylanbrc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 0 ∈ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) )
71 hmeocnvcn ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Homeo 𝐽 ) → ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
72 45 71 syl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
73 72 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
74 simprl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝑦 ⊆ 𝑋 )
75 49 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝑋 = ∪ 𝐽 )
76 74 75 sseqtrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝑦 ⊆ ∪ 𝐽 )
77 simprrr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( 𝐽 ↾t 𝑦 ) ∈ Conn )
78 43 73 76 77 connima ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( 𝐽 ↾t ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ) ∈ Conn )
79 4 conncompss ⊢ ( ( ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ⊆ 𝑋 ∧ 0 ∈ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ∧ ( 𝐽 ↾t ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ) ∈ Conn ) → ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ⊆ 𝑆 )
80 60 70 78 79 mp3an2i ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ⊆ 𝑆 )
81 eqid ⊢ ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) = ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) )
82 81 1 14 13 grplactcnv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
83 22 82 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ∧ ◡ ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) = ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ ( ( invg ‘ 𝐺 ) ‘ 𝐴 ) ) ) )
84 83 simpld ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 )
85 81 1 grplactfval ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) )
86 85 adantl ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) )
87 86 f1oeq1d ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑧 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ‘ 𝐴 ) : 𝑋 –1-1-onto→ 𝑋 ↔ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 ) )
88 84 87 mpbid ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
89 88 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
90 f1ocnv ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 → ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
91 f1ofun ⊢ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 → Fun ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) )
92 89 90 91 3syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → Fun ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) )
93 f1odm ⊢ ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 → dom ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) = 𝑋 )
94 89 90 93 3syl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → dom ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) = 𝑋 )
95 74 94 sseqtrrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝑦 ⊆ dom ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) )
96 funimass3 ⊢ ( ( Fun ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑦 ⊆ dom ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) ) → ( ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ⊆ 𝑆 ↔ 𝑦 ⊆ ( ◡ ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ) )
97 92 95 96 syl2anc ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → ( ( ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑦 ) ⊆ 𝑆 ↔ 𝑦 ⊆ ( ◡ ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) ) )
98 80 97 mpbid ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝑦 ⊆ ( ◡ ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
99 41 adantr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → [ 𝐴 ] ∼ = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
100 imacnvcnv ⊢ ( ◡ ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) = ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 )
101 99 100 eqtr4di ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → [ 𝐴 ] ∼ = ( ◡ ◡ ( 𝑧 ∈ 𝑋 ↦ ( 𝐴 ( +g ‘ 𝐺 ) 𝑧 ) ) “ 𝑆 ) )
102 98 101 sseqtrrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ⊆ 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) ) → 𝑦 ⊆ [ 𝐴 ] ∼ )
103 102 expr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ⊆ 𝑋 ) → ( ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) → 𝑦 ⊆ [ 𝐴 ] ∼ ) )
104 58 103 sylan2 ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝒫 𝑋 ) → ( ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) → 𝑦 ⊆ [ 𝐴 ] ∼ ) )
105 104 ralrimiva ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝒫 𝑋 ( ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) → 𝑦 ⊆ [ 𝐴 ] ∼ ) )
106 eleq2w ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
107 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t 𝑦 ) )
108 107 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐽 ↾t 𝑥 ) ∈ Conn ↔ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) )
109 106 108 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ↔ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
110 109 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦 ⊆ [ 𝐴 ] ∼ ↔ ∀ 𝑦 ∈ 𝒫 𝑋 ( ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) → 𝑦 ⊆ [ 𝐴 ] ∼ ) )
111 105 110 sylibr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦 ⊆ [ 𝐴 ] ∼ )
112 unissb ⊢ ( ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ [ 𝐴 ] ∼ ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦 ⊆ [ 𝐴 ] ∼ )
113 111 112 sylibr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ [ 𝐴 ] ∼ )
114 57 113 eqssd ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋 ) → [ 𝐴 ] ∼ = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )