Step | Hyp | Ref
| Expression |
1 | | symgtgp.g |
. . 3
⊢ 𝐺 = (SymGrp‘𝐴) |
2 | 1 | symggrp 18458 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp) |
3 | | grpmnd 18048 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd) |
5 | | eqid 2818 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 5 | symgtopn 18463 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) =
(TopOpen‘𝐺)) |
7 | | distopon 21533 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) |
8 | | eqid 2818 |
. . . . . . . 8
⊢
(∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴})) |
9 | 8 | pttoponconst 22133 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) |
10 | 7, 9 | mpdan 683 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) |
11 | 1, 5 | elsymgbas 18438 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
12 | | f1of 6608 |
. . . . . . . . 9
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴) |
13 | | elmapg 8408 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (𝐴 ↑m 𝐴) ↔ 𝑥:𝐴⟶𝐴)) |
14 | 13 | anidms 567 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝐴 ↑m 𝐴) ↔ 𝑥:𝐴⟶𝐴)) |
15 | 12, 14 | syl5ibr 247 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1-onto→𝐴 → 𝑥 ∈ (𝐴 ↑m 𝐴))) |
16 | 11, 15 | sylbid 241 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (𝐴 ↑m 𝐴))) |
17 | 16 | ssrdv 3970 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝐴 ↑m 𝐴)) |
18 | | resttopon 21697 |
. . . . . 6
⊢
(((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴)) ∧ (Base‘𝐺) ⊆ (𝐴 ↑m 𝐴)) → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) ∈
(TopOn‘(Base‘𝐺))) |
19 | 10, 17, 18 | syl2anc 584 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) ∈
(TopOn‘(Base‘𝐺))) |
20 | 6, 19 | eqeltrrd 2911 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺))) |
21 | | eqid 2818 |
. . . . 5
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
22 | 5, 21 | istps 21470 |
. . . 4
⊢ (𝐺 ∈ TopSp ↔
(TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
23 | 20, 22 | sylibr 235 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopSp) |
24 | | eqid 2818 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
25 | 1, 5, 24 | symgplusg 18445 |
. . . . . . 7
⊢
(+g‘𝐺) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 ∘ 𝑦)) |
26 | | eqid 2818 |
. . . . . . . 8
⊢
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺)) = ((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝐺)) |
27 | | distop 21531 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
28 | | eqid 2818 |
. . . . . . . . . 10
⊢
(𝒫 𝐴
↑ko 𝒫 𝐴) = (𝒫 𝐴 ↑ko 𝒫 𝐴) |
29 | 28 | xkotopon 22136 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ Top) → (𝒫 𝐴 ↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) |
30 | 27, 27, 29 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) |
31 | | cndis 21827 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑m 𝐴)) |
32 | 7, 31 | mpdan 683 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑m 𝐴)) |
33 | 17, 32 | sseqtrrd 4005 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) |
34 | | disllycmp 22034 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Locally Comp) |
35 | | llynlly 22013 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∈
Locally Comp → 𝒫 𝐴 ∈ 𝑛-Locally
Comp) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ 𝑛-Locally
Comp) |
37 | | eqid 2818 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) |
38 | 37 | xkococn 22196 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ 𝑛-Locally Comp ∧ 𝒫 𝐴 ∈ Top) → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ↑ko 𝒫 𝐴) ×t (𝒫
𝐴 ↑ko
𝒫 𝐴)) Cn (𝒫
𝐴 ↑ko
𝒫 𝐴))) |
39 | 27, 36, 27, 38 | syl3anc 1363 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ↑ko 𝒫 𝐴) ×t (𝒫
𝐴 ↑ko
𝒫 𝐴)) Cn (𝒫
𝐴 ↑ko
𝒫 𝐴))) |
40 | 26, 30, 33, 26, 30, 33, 39 | cnmpt2res 22213 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 ∘ 𝑦)) ∈ ((((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴))) |
41 | 25, 40 | eqeltrid 2914 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ ((((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴))) |
42 | | xkopt 22191 |
. . . . . . . . . . 11
⊢
((𝒫 𝐴 ∈
Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 ↑ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) |
43 | 27, 42 | mpancom 684 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑ko 𝒫 𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) |
44 | 43 | oveq1d 7160 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺))) |
45 | 44, 6 | eqtrd 2853 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺)) =
(TopOpen‘𝐺)) |
46 | 45, 45 | oveq12d 7163 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))) =
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) |
47 | 46 | oveq1d 7160 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ((((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴)) = (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴))) |
48 | 41, 47 | eleqtrd 2912 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴))) |
49 | | vex 3495 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
50 | | vex 3495 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
51 | 49, 50 | coex 7624 |
. . . . . . . . . . 11
⊢ (𝑥 ∘ 𝑦) ∈ V |
52 | 25, 51 | fnmpoi 7757 |
. . . . . . . . . 10
⊢
(+g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) |
53 | | eqid 2818 |
. . . . . . . . . . 11
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
54 | 5, 24, 53 | plusfeq 17848 |
. . . . . . . . . 10
⊢
((+g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (+𝑓‘𝐺) = (+g‘𝐺)) |
55 | 52, 54 | ax-mp 5 |
. . . . . . . . 9
⊢
(+𝑓‘𝐺) = (+g‘𝐺) |
56 | 55 | eqcomi 2827 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+𝑓‘𝐺) |
57 | 5, 56 | grpplusf 18053 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
(+g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
58 | | frn 6513 |
. . . . . . 7
⊢
((+g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → ran (+g‘𝐺) ⊆ (Base‘𝐺)) |
59 | 2, 57, 58 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ran (+g‘𝐺) ⊆ (Base‘𝐺)) |
60 | | cnrest2 21822 |
. . . . . 6
⊢
(((𝒫 𝐴
↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (+g‘𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴)) ↔ (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
61 | 30, 59, 33, 60 | syl3anc 1363 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴)) ↔ (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
62 | 48, 61 | mpbid 233 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺)))) |
63 | 45 | oveq2d 7161 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn ((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝐺))) =
(((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
64 | 62, 63 | eleqtrd 2912 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(TopOpen‘𝐺))) |
65 | 56, 21 | istmd 22610 |
. . 3
⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧
(+g‘𝐺)
∈ (((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))) |
66 | 4, 23, 64, 65 | syl3anbrc 1335 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopMnd) |
67 | | id 22 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
68 | | fconst6g 6561 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Top → (𝐴 ×
{𝒫 𝐴}):𝐴⟶Top) |
69 | 27, 68 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 × {𝒫 𝐴}):𝐴⟶Top) |
70 | 11 | biimpa 477 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) |
71 | | f1ocnv 6620 |
. . . . . . . . . . . 12
⊢ (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴) |
72 | | f1of 6608 |
. . . . . . . . . . . 12
⊢ (◡𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴⟶𝐴) |
73 | 70, 71, 72 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥:𝐴⟶𝐴) |
74 | 73 | ffvelrnda 6843 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑦 ∈ 𝐴) → (◡𝑥‘𝑦) ∈ 𝐴) |
75 | 74 | an32s 648 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥‘𝑦) ∈ 𝐴) |
76 | 75 | fmpttd 6871 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴) |
77 | 76 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴) |
78 | | cnveq 5737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑓 → ◡𝑥 = ◡𝑓) |
79 | 78 | fveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑓 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦)) |
80 | | eqid 2818 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) |
81 | | fvex 6676 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑓‘𝑦) ∈ V |
82 | 79, 80, 81 | fvmpt 6761 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦)) |
83 | 82 | ad2antlr 723 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦)) |
84 | 83 | eleq1d 2894 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡)) |
85 | | eqid 2818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) |
86 | 85 | mptiniseg 6086 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ V → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) |
87 | 86 | elv 3497 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} |
88 | | eqid 2818 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) |
89 | 10 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) |
90 | 17 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (Base‘𝐺) ⊆ (𝐴 ↑m 𝐴)) |
91 | | toponuni 21450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴)) → (𝐴 ↑m 𝐴) = ∪
(∏t‘(𝐴 × {𝒫 𝐴}))) |
92 | | mpteq1 5145 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ↑m 𝐴) = ∪
(∏t‘(𝐴 × {𝒫 𝐴})) → (𝑢 ∈ (𝐴 ↑m 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦)))) |
93 | 89, 91, 92 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑m 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦)))) |
94 | | simpll 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝐴 ∈ 𝑉) |
95 | 69 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝐴 × {𝒫 𝐴}):𝐴⟶Top) |
96 | 1, 5 | elsymgbas 18438 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ 𝑉 → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴)) |
97 | 96 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴)) |
98 | 97 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓:𝐴–1-1-onto→𝐴) |
99 | | f1ocnv 6620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→𝐴) |
100 | | f1of 6608 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴⟶𝐴) |
101 | 98, 99, 100 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ◡𝑓:𝐴⟶𝐴) |
102 | | simplr 765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑦 ∈ 𝐴) |
103 | 101, 102 | ffvelrnd 6844 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴) |
104 | | eqid 2818 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) = ∪
(∏t‘(𝐴 × {𝒫 𝐴})) |
105 | 104, 8 | ptpjcn 22147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝒫 𝐴}):𝐴⟶Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)))) |
106 | 94, 95, 103, 105 | syl3anc 1363 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)))) |
107 | 27 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ Top) |
108 | | fvconst2g 6956 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((𝒫 𝐴 ∈
Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴) |
109 | 107, 103,
108 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴) |
110 | 109 | oveq2d 7161 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦))) = ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) |
111 | 106, 110 | eleqtrd 2912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) |
112 | 93, 111 | eqeltrd 2910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑m 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) |
113 | 88, 89, 90, 112 | cnmpt1res 22212 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴)) |
114 | 6 | oveq1d 7160 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ 𝑉 → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴) =
((TopOpen‘𝐺) Cn
𝒫 𝐴)) |
115 | 114 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴) =
((TopOpen‘𝐺) Cn
𝒫 𝐴)) |
116 | 113, 115 | eleqtrd 2912 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴)) |
117 | | snelpwi 5327 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) |
118 | 117 | ad2antlr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑦} ∈ 𝒫 𝐴) |
119 | | cnima 21801 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ∧ {𝑦} ∈ 𝒫 𝐴) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺)) |
120 | 116, 118,
119 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺)) |
121 | 87, 120 | eqeltrrid 2915 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺)) |
122 | 121 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺)) |
123 | | fveq1 6662 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑓 → (𝑢‘(◡𝑓‘𝑦)) = (𝑓‘(◡𝑓‘𝑦))) |
124 | 123 | eqeq1d 2820 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑓 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑓‘(◡𝑓‘𝑦)) = 𝑦)) |
125 | | simplr 765 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ (Base‘𝐺)) |
126 | 98 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓:𝐴–1-1-onto→𝐴) |
127 | | simpllr 772 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑦 ∈ 𝐴) |
128 | | f1ocnvfv2 7025 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦) |
129 | 126, 127,
128 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦) |
130 | 124, 125,
129 | elrabd 3679 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) |
131 | | ssrab2 4053 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺)) |
133 | 11 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
134 | 133 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) |
135 | 103 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴) |
136 | | f1ocnvfv 7026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥:𝐴–1-1-onto→𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))) |
137 | 134, 135,
136 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))) |
138 | | simplrr 774 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝑡) |
139 | | eleq1 2897 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → ((◡𝑥‘𝑦) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡)) |
140 | 138, 139 | syl5ibrcom 248 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → (◡𝑥‘𝑦) ∈ 𝑡)) |
141 | 137, 140 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) |
142 | 141 | ralrimiva 3179 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) |
143 | | fveq1 6662 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑥 → (𝑢‘(◡𝑓‘𝑦)) = (𝑥‘(◡𝑓‘𝑦))) |
144 | 143 | eqeq1d 2820 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑥 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑥‘(◡𝑓‘𝑦)) = 𝑦)) |
145 | 144 | ralrab 3682 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
{𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) |
146 | 142, 145 | sylibr 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡) |
147 | | ssrab 4046 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} ↔ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) ∧ ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡)) |
148 | 132, 146,
147 | sylanbrc 583 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡}) |
149 | 80 | mptpreima 6085 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡) = {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} |
150 | 148, 149 | sseqtrrdi 4015 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡)) |
151 | | funmpt 6386 |
. . . . . . . . . . . . . . . 16
⊢ Fun
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) |
152 | | fvex 6676 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑥‘𝑦) ∈ V |
153 | 152, 80 | dmmpti 6485 |
. . . . . . . . . . . . . . . . 17
⊢ dom
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (Base‘𝐺) |
154 | 132, 153 | sseqtrrdi 4015 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) |
155 | | funimass3 6816 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∧ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))) |
156 | 151, 154,
155 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))) |
157 | 150, 156 | mpbird 258 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡) |
158 | | eleq2 2898 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (𝑓 ∈ 𝑣 ↔ 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})) |
159 | | imaeq2 5918 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) = ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})) |
160 | 159 | sseq1d 3995 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡 ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) |
161 | 158, 160 | anbi12d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡) ↔ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡))) |
162 | 161 | rspcev 3620 |
. . . . . . . . . . . . . 14
⊢ (({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺) ∧ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)) |
163 | 122, 130,
157, 162 | syl12anc 832 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)) |
164 | 163 | expr 457 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((◡𝑓‘𝑦) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) |
165 | 84, 164 | sylbid 241 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) |
166 | 165 | ralrimiva 3179 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) |
167 | 20 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺))) |
168 | 7 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ (TopOn‘𝐴)) |
169 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓 ∈ (Base‘𝐺)) |
170 | | iscnp 21773 |
. . . . . . . . . . 11
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))))) |
171 | 167, 168,
169, 170 | syl3anc 1363 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))))) |
172 | 77, 166, 171 | mpbir2and 709 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)) |
173 | 172 | ralrimiva 3179 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)) |
174 | | cncnp 21816 |
. . . . . . . . . 10
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) |
175 | 20, 7, 174 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) |
176 | 175 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) |
177 | 76, 173, 176 | mpbir2and 709 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴)) |
178 | | fvconst2g 6956 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴) |
179 | 27, 178 | sylan 580 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴) |
180 | 179 | oveq2d 7161 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)) = ((TopOpen‘𝐺) Cn 𝒫 𝐴)) |
181 | 177, 180 | eleqtrrd 2913 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦))) |
182 | 8, 20, 67, 69, 181 | ptcn 22163 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) ∈ ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴})))) |
183 | | eqid 2818 |
. . . . . . . . 9
⊢
(invg‘𝐺) = (invg‘𝐺) |
184 | 5, 183 | grpinvf 18088 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
185 | 2, 184 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
186 | 185 | feqmptd 6726 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥))) |
187 | 1, 5, 183 | symginv 18460 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝐺) →
((invg‘𝐺)‘𝑥) = ◡𝑥) |
188 | 187 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = ◡𝑥) |
189 | 73 | feqmptd 6726 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥 = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) |
190 | 188, 189 | eqtrd 2853 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) |
191 | 190 | mpteq2dva 5152 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))) |
192 | 186, 191 | eqtrd 2853 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))) |
193 | 43 | oveq2d 7161 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫 𝐴)) = ((TopOpen‘𝐺) Cn
(∏t‘(𝐴 × {𝒫 𝐴})))) |
194 | 182, 192,
193 | 3eltr4d 2925 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴))) |
195 | | frn 6513 |
. . . . . 6
⊢
((invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺) → ran (invg‘𝐺) ⊆ (Base‘𝐺)) |
196 | 2, 184, 195 | 3syl 18 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ran (invg‘𝐺) ⊆ (Base‘𝐺)) |
197 | | cnrest2 21822 |
. . . . 5
⊢
(((𝒫 𝐴
↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (invg‘𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴)) ↔
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn ((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
198 | 30, 196, 33, 197 | syl3anc 1363 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴)) ↔
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn ((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
199 | 194, 198 | mpbid 233 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝐺)))) |
200 | 45 | oveq2d 7161 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))) =
((TopOpen‘𝐺) Cn
(TopOpen‘𝐺))) |
201 | 199, 200 | eleqtrd 2912 |
. 2
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))) |
202 | 21, 183 | istgp 22613 |
. 2
⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺)))) |
203 | 2, 66, 201, 202 | syl3anbrc 1335 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp) |