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

Theorem tgpconncompeqg 22863
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.
StepHypRef Expression
1 dfec2 8323 . . . . 5 (𝐴𝑋 → [𝐴] = {𝑧𝐴 𝑧})
21adantl 485 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = {𝑧𝐴 𝑧})
3 tgpconncomp.s . . . . . . . . 9 𝑆 = {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}
4 ssrab2 3969 . . . . . . . . . 10 {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋
5 sspwuni 4985 . . . . . . . . . 10 ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝒫 𝑋 {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝑋)
64, 5mpbi 233 . . . . . . . . 9 {𝑥 ∈ 𝒫 𝑋 ∣ ( 0𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ 𝑋
73, 6eqsstri 3911 . . . . . . . 8 𝑆𝑋
87a1i 11 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝑆𝑋)
9 tgpconncomp.x . . . . . . . 8 𝑋 = (Base‘𝐺)
10 eqid 2738 . . . . . . . 8 (invg𝐺) = (invg𝐺)
11 eqid 2738 . . . . . . . 8 (+g𝐺) = (+g𝐺)
12 tgpconncompeqg.r . . . . . . . 8 = (𝐺 ~QG 𝑆)
139, 10, 11, 12eqgval 18447 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝑆𝑋) → (𝐴 𝑧 ↔ (𝐴𝑋𝑧𝑋 ∧ (((invg𝐺)‘𝐴)(+g𝐺)𝑧) ∈ 𝑆)))
148, 13syldan 594 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐴 𝑧 ↔ (𝐴𝑋𝑧𝑋 ∧ (((invg𝐺)‘𝐴)(+g𝐺)𝑧) ∈ 𝑆)))
15 simp2 1138 . . . . . 6 ((𝐴𝑋𝑧𝑋 ∧ (((invg𝐺)‘𝐴)(+g𝐺)𝑧) ∈ 𝑆) → 𝑧𝑋)
1614, 15syl6bi 256 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐴 𝑧𝑧𝑋))
1716abssdv 3958 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → {𝑧𝐴 𝑧} ⊆ 𝑋)
182, 17eqsstrd 3915 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] 𝑋)
19 simpr 488 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐴𝑋)
20 tgpgrp 22829 . . . . . . 7 (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
21 tgpconncomp.z . . . . . . . 8 0 = (0g𝐺)
229, 11, 21, 10grplinv 18270 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝐴𝑋) → (((invg𝐺)‘𝐴)(+g𝐺)𝐴) = 0 )
2320, 22sylan 583 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (((invg𝐺)‘𝐴)(+g𝐺)𝐴) = 0 )
24 tgpconncomp.j . . . . . . . . 9 𝐽 = (TopOpen‘𝐺)
2524, 9tgptopon 22833 . . . . . . . 8 (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
2625adantr 484 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐽 ∈ (TopOn‘𝑋))
2720adantr 484 . . . . . . . 8 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐺 ∈ Grp)
289, 21grpidcl 18249 . . . . . . . 8 (𝐺 ∈ Grp → 0𝑋)
2927, 28syl 17 . . . . . . 7 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 0𝑋)
303conncompid 22182 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 0𝑋) → 0𝑆)
3126, 29, 30syl2anc 587 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 0𝑆)
3223, 31eqeltrd 2833 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (((invg𝐺)‘𝐴)(+g𝐺)𝐴) ∈ 𝑆)
339, 10, 11, 12eqgval 18447 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝑆𝑋) → (𝐴 𝐴 ↔ (𝐴𝑋𝐴𝑋 ∧ (((invg𝐺)‘𝐴)(+g𝐺)𝐴) ∈ 𝑆)))
348, 33syldan 594 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐴 𝐴 ↔ (𝐴𝑋𝐴𝑋 ∧ (((invg𝐺)‘𝐴)(+g𝐺)𝐴) ∈ 𝑆)))
3519, 19, 32, 34mpbir3and 1343 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐴 𝐴)
36 elecg 8363 . . . . 5 ((𝐴𝑋𝐴𝑋) → (𝐴 ∈ [𝐴] 𝐴 𝐴))
3719, 19, 36syl2anc 587 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐴 ∈ [𝐴] 𝐴 𝐴))
3835, 37mpbird 260 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝐴 ∈ [𝐴] )
399, 12, 11eqglact 18449 . . . . . . 7 ((𝐺 ∈ Grp ∧ 𝑆𝑋𝐴𝑋) → [𝐴] = ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆))
407, 39mp3an2 1450 . . . . . 6 ((𝐺 ∈ Grp ∧ 𝐴𝑋) → [𝐴] = ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆))
4120, 40sylan 583 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆))
4241oveq2d 7186 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐽t [𝐴] ) = (𝐽t ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆)))
43 eqid 2738 . . . . 5 𝐽 = 𝐽
44 eqid 2738 . . . . . . 7 (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) = (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧))
4544, 9, 11, 24tgplacthmeo 22854 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽Homeo𝐽))
46 hmeocn 22511 . . . . . 6 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
4745, 46syl 17 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
48 toponuni 21665 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
4926, 48syl 17 . . . . . 6 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝑋 = 𝐽)
507, 49sseqtrid 3929 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → 𝑆 𝐽)
513conncompconn 22183 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 0𝑋) → (𝐽t 𝑆) ∈ Conn)
5226, 29, 51syl2anc 587 . . . . 5 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐽t 𝑆) ∈ Conn)
5343, 47, 50, 52connima 22176 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐽t ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆)) ∈ Conn)
5442, 53eqeltrd 2833 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐽t [𝐴] ) ∈ Conn)
55 eqid 2738 . . . 4 {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} = {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}
5655conncompss 22184 . . 3 (([𝐴] 𝑋𝐴 ∈ [𝐴] ∧ (𝐽t [𝐴] ) ∈ Conn) → [𝐴] {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
5718, 38, 54, 56syl3anc 1372 . 2 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
58 elpwi 4497 . . . . . 6 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
5944mptpreima 6070 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) = {𝑧𝑋 ∣ (𝐴(+g𝐺)𝑧) ∈ 𝑦}
6059ssrab3 3971 . . . . . . . . . 10 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ⊆ 𝑋
6129adantr 484 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 0𝑋)
629, 11, 21grprid 18252 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝐴𝑋) → (𝐴(+g𝐺) 0 ) = 𝐴)
6320, 62sylan 583 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝐴(+g𝐺) 0 ) = 𝐴)
6463adantr 484 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (𝐴(+g𝐺) 0 ) = 𝐴)
65 simprrl 781 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝐴𝑦)
6664, 65eqeltrd 2833 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (𝐴(+g𝐺) 0 ) ∈ 𝑦)
67 oveq2 7178 . . . . . . . . . . . . 13 (𝑧 = 0 → (𝐴(+g𝐺)𝑧) = (𝐴(+g𝐺) 0 ))
6867eleq1d 2817 . . . . . . . . . . . 12 (𝑧 = 0 → ((𝐴(+g𝐺)𝑧) ∈ 𝑦 ↔ (𝐴(+g𝐺) 0 ) ∈ 𝑦))
6968, 59elrab2 3591 . . . . . . . . . . 11 ( 0 ∈ ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ↔ ( 0𝑋 ∧ (𝐴(+g𝐺) 0 ) ∈ 𝑦))
7061, 66, 69sylanbrc 586 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 0 ∈ ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦))
71 hmeocnvcn 22512 . . . . . . . . . . . . 13 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
7245, 71syl 17 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
7372adantr 484 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∈ (𝐽 Cn 𝐽))
74 simprl 771 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝑦𝑋)
7549adantr 484 . . . . . . . . . . . 12 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝑋 = 𝐽)
7674, 75sseqtrd 3917 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝑦 𝐽)
77 simprrr 782 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (𝐽t 𝑦) ∈ Conn)
7843, 73, 76, 77connima 22176 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (𝐽t ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦)) ∈ Conn)
793conncompss 22184 . . . . . . . . . 10 ((((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ⊆ 𝑋0 ∈ ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ∧ (𝐽t ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦)) ∈ Conn) → ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
8060, 70, 78, 79mp3an2i 1467 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ⊆ 𝑆)
81 eqid 2738 . . . . . . . . . . . . . . . 16 (𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧))) = (𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))
8281, 9, 11, 10grplactcnv 18320 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ 𝐴𝑋) → (((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴):𝑋1-1-onto𝑋((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴) = ((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘((invg𝐺)‘𝐴))))
8320, 82sylan 583 . . . . . . . . . . . . . 14 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴):𝑋1-1-onto𝑋((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴) = ((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘((invg𝐺)‘𝐴))))
8483simpld 498 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴):𝑋1-1-onto𝑋)
8581, 9grplactfval 18318 . . . . . . . . . . . . . . 15 (𝐴𝑋 → ((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴) = (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)))
8685adantl 485 . . . . . . . . . . . . . 14 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴) = (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)))
8786f1oeq1d 6613 . . . . . . . . . . . . 13 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (((𝑔𝑋 ↦ (𝑧𝑋 ↦ (𝑔(+g𝐺)𝑧)))‘𝐴):𝑋1-1-onto𝑋 ↔ (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋))
8884, 87mpbid 235 . . . . . . . . . . . 12 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋)
8988adantr 484 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋)
90 f1ocnv 6630 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋(𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋)
91 f1ofun 6620 . . . . . . . . . . 11 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋 → Fun (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)))
9289, 90, 913syl 18 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → Fun (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)))
93 f1odm 6622 . . . . . . . . . . . 12 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)):𝑋1-1-onto𝑋 → dom (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) = 𝑋)
9489, 90, 933syl 18 . . . . . . . . . . 11 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → dom (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) = 𝑋)
9574, 94sseqtrrd 3918 . . . . . . . . . 10 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝑦 ⊆ dom (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)))
96 funimass3 6831 . . . . . . . . . 10 ((Fun (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) ∧ 𝑦 ⊆ dom (𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧))) → (((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ⊆ 𝑆𝑦 ⊆ ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆)))
9792, 95, 96syl2anc 587 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → (((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑦) ⊆ 𝑆𝑦 ⊆ ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆)))
9880, 97mpbid 235 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝑦 ⊆ ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆))
9941adantr 484 . . . . . . . . 9 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → [𝐴] = ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆))
100 imacnvcnv 6038 . . . . . . . . 9 ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆) = ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆)
10199, 100eqtr4di 2791 . . . . . . . 8 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → [𝐴] = ((𝑧𝑋 ↦ (𝐴(+g𝐺)𝑧)) “ 𝑆))
10298, 101sseqtrrd 3918 . . . . . . 7 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ (𝑦𝑋 ∧ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn))) → 𝑦 ⊆ [𝐴] )
103102expr 460 . . . . . 6 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ 𝑦𝑋) → ((𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ))
10458, 103sylan2 596 . . . . 5 (((𝐺 ∈ TopGrp ∧ 𝐴𝑋) ∧ 𝑦 ∈ 𝒫 𝑋) → ((𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ))
105104ralrimiva 3096 . . . 4 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ∀𝑦 ∈ 𝒫 𝑋((𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ))
106 eleq2w 2816 . . . . . 6 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
107 oveq2 7178 . . . . . . 7 (𝑥 = 𝑦 → (𝐽t 𝑥) = (𝐽t 𝑦))
108107eleq1d 2817 . . . . . 6 (𝑥 = 𝑦 → ((𝐽t 𝑥) ∈ Conn ↔ (𝐽t 𝑦) ∈ Conn))
109106, 108anbi12d 634 . . . . 5 (𝑥 = 𝑦 → ((𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn) ↔ (𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn)))
110109ralrab 3593 . . . 4 (∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] ↔ ∀𝑦 ∈ 𝒫 𝑋((𝐴𝑦 ∧ (𝐽t 𝑦) ∈ Conn) → 𝑦 ⊆ [𝐴] ))
111105, 110sylibr 237 . . 3 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] )
112 unissb 4830 . . 3 ( {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ [𝐴] ↔ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)}𝑦 ⊆ [𝐴] )
113111, 112sylibr 237 . 2 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)} ⊆ [𝐴] )
11457, 113eqssd 3894 1 ((𝐺 ∈ TopGrp ∧ 𝐴𝑋) → [𝐴] = {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴𝑥 ∧ (𝐽t 𝑥) ∈ Conn)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2114  {cab 2716  wral 3053  {crab 3057  wss 3843  𝒫 cpw 4488   cuni 4796   class class class wbr 5030  cmpt 5110  ccnv 5524  dom cdm 5525  cima 5528  Fun wfun 6333  1-1-ontowf1o 6338  cfv 6339  (class class class)co 7170  [cec 8318  Basecbs 16586  +gcplusg 16668  t crest 16797  TopOpenctopn 16798  0gc0g 16816  Grpcgrp 18219  invgcminusg 18220   ~QG cqg 18393  TopOnctopon 21661   Cn ccn 21975  Conncconn 22162  Homeochmeo 22504  TopGrpctgp 22822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-ec 8322  df-map 8439  df-en 8556  df-fin 8559  df-fi 8948  df-rest 16799  df-0g 16818  df-topgen 16820  df-plusf 17967  df-mgm 17968  df-sgrp 18017  df-mnd 18028  df-grp 18222  df-minusg 18223  df-eqg 18396  df-top 21645  df-topon 21662  df-topsp 21684  df-bases 21697  df-cld 21770  df-cn 21978  df-cnp 21979  df-conn 22163  df-tx 22313  df-hmeo 22506  df-tmd 22823  df-tgp 22824
This theorem is referenced by:  tgpconncomp  22864
  Copyright terms: Public domain W3C validator