Step | Hyp | Ref
| Expression |
1 | | dfec2 7632 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧}) |
2 | 1 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = {𝑧 ∣ 𝐴 ∼ 𝑧}) |
3 | | tgpconcomp.s |
. . . . . . . . 9
⊢ 𝑆 = ∪
{𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} |
4 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝒫 𝑋 |
5 | | sspwuni 4547 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝒫 𝑋 ↔ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝑋) |
6 | 4, 5 | mpbi 219 |
. . . . . . . . 9
⊢ ∪ {𝑥
∈ 𝒫 𝑋 ∣
( 0
∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ 𝑋 |
7 | 3, 6 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑆 ⊆ 𝑋 |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ 𝑋) |
9 | | tgpconcomp.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
10 | | eqid 2610 |
. . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) |
11 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
12 | | tgpconcompeqg.r |
. . . . . . . 8
⊢ ∼ =
(𝐺 ~QG
𝑆) |
13 | 9, 10, 11, 12 | eqgval 17466 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆))) |
14 | 8, 13 | syldan 486 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 ↔ (𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆))) |
15 | | simp2 1055 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝑧) ∈ 𝑆) → 𝑧 ∈ 𝑋) |
16 | 14, 15 | syl6bi 242 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝑧 → 𝑧 ∈ 𝑋)) |
17 | 16 | abssdv 3639 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → {𝑧 ∣ 𝐴 ∼ 𝑧} ⊆ 𝑋) |
18 | 2, 17 | eqsstrd 3602 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ 𝑋) |
19 | | simpr 476 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
20 | | tgpgrp 21692 |
. . . . . . 7
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
21 | | tgpconcomp.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
22 | 9, 11, 21, 10 | grplinv 17291 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 ) |
23 | 20, 22 | sylan 487 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) = 0 ) |
24 | | tgpconcomp.j |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝐺) |
25 | 24, 9 | tgptopon 21696 |
. . . . . . . 8
⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
27 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐺 ∈ Grp) |
28 | 9, 21 | grpidcl 17273 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑋) |
30 | 3 | concompid 21044 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → 0 ∈ 𝑆) |
31 | 26, 29, 30 | syl2anc 691 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 0 ∈ 𝑆) |
32 | 23, 31 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆) |
33 | 9, 10, 11, 12 | eqgval 17466 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆))) |
34 | 8, 33 | syldan 486 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∼ 𝐴 ↔ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐴)(+g‘𝐺)𝐴) ∈ 𝑆))) |
35 | 19, 19, 32, 34 | mpbir3and 1238 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∼ 𝐴) |
36 | | elecg 7672 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
37 | 19, 19, 36 | syl2anc 691 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ [𝐴] ∼ ↔ 𝐴 ∼ 𝐴)) |
38 | 35, 37 | mpbird 246 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴] ∼ ) |
39 | 9, 12, 11 | eqglact 17468 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) |
40 | 7, 39 | mp3an2 1404 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) |
41 | 20, 40 | sylan 487 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) |
42 | 41 | oveq2d 6565 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) = (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))) |
43 | | eqid 2610 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
44 | | eqid 2610 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) |
45 | 44, 9, 11, 24 | tgplacthmeo 21717 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽)) |
46 | | hmeocn 21373 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
47 | 45, 46 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
48 | | toponuni 20542 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
49 | 26, 48 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑋 = ∪ 𝐽) |
50 | 7, 49 | syl5sseq 3616 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝑆 ⊆ ∪ 𝐽) |
51 | 3 | concompcon 21045 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 0 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Con) |
52 | 26, 29, 51 | syl2anc 691 |
. . . . 5
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Con) |
53 | 43, 47, 50, 52 | conima 21038 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) ∈ Con) |
54 | 42, 53 | eqeltrd 2688 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t [𝐴] ∼ ) ∈
Con) |
55 | | eqid 2610 |
. . . 4
⊢ ∪ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} = ∪
{𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} |
56 | 55 | concompss 21046 |
. . 3
⊢ (([𝐴] ∼ ⊆ 𝑋 ∧ 𝐴 ∈ [𝐴] ∼ ∧ (𝐽 ↾t [𝐴] ∼ ) ∈ Con)
→ [𝐴] ∼
⊆ ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |
57 | 18, 38, 54, 56 | syl3anc 1318 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ ⊆ ∪ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |
58 | | elpwi 4117 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
59 | 44 | mptpreima 5545 |
. . . . . . . . . . . 12
⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) = {𝑧 ∈ 𝑋 ∣ (𝐴(+g‘𝐺)𝑧) ∈ 𝑦} |
60 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ 𝑋 ∣ (𝐴(+g‘𝐺)𝑧) ∈ 𝑦} ⊆ 𝑋 |
61 | 59, 60 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋 |
62 | 61 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋) |
63 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 0 ∈ 𝑋) |
64 | 9, 11, 21 | grprid 17276 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴) |
65 | 20, 64 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝐴(+g‘𝐺) 0 ) = 𝐴) |
66 | 65 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (𝐴(+g‘𝐺) 0 ) = 𝐴) |
67 | | simprrl 800 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝐴 ∈ 𝑦) |
68 | 66, 67 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (𝐴(+g‘𝐺) 0 ) ∈ 𝑦) |
69 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝐴(+g‘𝐺)𝑧) = (𝐴(+g‘𝐺) 0 )) |
70 | 69 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → ((𝐴(+g‘𝐺)𝑧) ∈ 𝑦 ↔ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦)) |
71 | 70, 59 | elrab2 3333 |
. . . . . . . . . . 11
⊢ ( 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ↔ ( 0 ∈ 𝑋 ∧ (𝐴(+g‘𝐺) 0 ) ∈ 𝑦)) |
72 | 63, 68, 71 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) |
73 | | hmeocnvcn 21374 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽Homeo𝐽) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
74 | 45, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
75 | 74 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∈ (𝐽 Cn 𝐽)) |
76 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝑦 ⊆ 𝑋) |
77 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝑋 = ∪ 𝐽) |
78 | 76, 77 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝑦 ⊆ ∪ 𝐽) |
79 | | simprrr 801 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (𝐽 ↾t 𝑦) ∈ Con) |
80 | 43, 75, 78, 79 | conima 21038 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Con) |
81 | 3 | concompss 21046 |
. . . . . . . . . 10
⊢ (((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑋 ∧ 0 ∈ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ∧ (𝐽 ↾t (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦)) ∈ Con) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆) |
82 | 62, 72, 80, 81 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆) |
83 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧))) = (𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧))) |
84 | 83, 9, 11, 10 | grplactcnv 17341 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘((invg‘𝐺)‘𝐴)))) |
85 | 20, 84 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘((invg‘𝐺)‘𝐴)))) |
86 | 85 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋) |
87 | 83, 9 | grplactfval 17339 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑋 → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) |
89 | | f1oeq1 6040 |
. . . . . . . . . . . . . 14
⊢ (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴) = (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (((𝑔 ∈ 𝑋 ↦ (𝑧 ∈ 𝑋 ↦ (𝑔(+g‘𝐺)𝑧)))‘𝐴):𝑋–1-1-onto→𝑋 ↔ (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋)) |
91 | 86, 90 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
92 | 91 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → (𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
93 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋) |
94 | | f1ofun 6052 |
. . . . . . . . . . 11
⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) |
95 | 92, 93, 94 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → Fun ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) |
96 | | f1odm 6054 |
. . . . . . . . . . . 12
⊢ (◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)):𝑋–1-1-onto→𝑋 → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋) |
97 | 92, 93, 96 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) = 𝑋) |
98 | 76, 97 | sseqtr4d 3605 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) |
99 | | funimass3 6241 |
. . . . . . . . . 10
⊢ ((Fun
◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) ∧ 𝑦 ⊆ dom ◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))) |
100 | 95, 98, 99 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → ((◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑦) ⊆ 𝑆 ↔ 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆))) |
101 | 82, 100 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝑦 ⊆ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) |
102 | 41 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → [𝐴] ∼ = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) |
103 | | imacnvcnv 5517 |
. . . . . . . . 9
⊢ (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆) = ((𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆) |
104 | 102, 103 | syl6eqr 2662 |
. . . . . . . 8
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → [𝐴] ∼ = (◡◡(𝑧 ∈ 𝑋 ↦ (𝐴(+g‘𝐺)𝑧)) “ 𝑆)) |
105 | 101, 104 | sseqtr4d 3605 |
. . . . . . 7
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ (𝑦 ⊆ 𝑋 ∧ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) → 𝑦 ⊆ [𝐴] ∼ ) |
106 | 105 | expr 641 |
. . . . . 6
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ⊆ 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con) → 𝑦 ⊆ [𝐴] ∼ )) |
107 | 58, 106 | sylan2 490 |
. . . . 5
⊢ (((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) ∧ 𝑦 ∈ 𝒫 𝑋) → ((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con) → 𝑦 ⊆ [𝐴] ∼ )) |
108 | 107 | ralrimiva 2949 |
. . . 4
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ 𝒫 𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con) → 𝑦 ⊆ [𝐴] ∼ )) |
109 | | eleq2 2677 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦)) |
110 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐽 ↾t 𝑥) = (𝐽 ↾t 𝑦)) |
111 | 110 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐽 ↾t 𝑥) ∈ Con ↔ (𝐽 ↾t 𝑦) ∈ Con)) |
112 | 109, 111 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con) ↔ (𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con))) |
113 | 112 | ralrab 3335 |
. . . 4
⊢
(∀𝑦 ∈
{𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}𝑦 ⊆ [𝐴] ∼ ↔
∀𝑦 ∈ 𝒫
𝑋((𝐴 ∈ 𝑦 ∧ (𝐽 ↾t 𝑦) ∈ Con) → 𝑦 ⊆ [𝐴] ∼ )) |
114 | 108, 113 | sylibr 223 |
. . 3
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}𝑦 ⊆ [𝐴] ∼ ) |
115 | | unissb 4405 |
. . 3
⊢ (∪ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ [𝐴] ∼ ↔
∀𝑦 ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}𝑦 ⊆ [𝐴] ∼ ) |
116 | 114, 115 | sylibr 223 |
. 2
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⊆ [𝐴] ∼ ) |
117 | 57, 116 | eqssd 3585 |
1
⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥
∈ 𝒫 𝑋 ∣
(𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)}) |