Step | Hyp | Ref
| Expression |
1 | | symgtgp.g |
. . 3
⊢ 𝐺 = (SymGrp‘𝐴) |
2 | 1 | symggrp 17643 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp) |
3 | | grpmnd 17252 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd) |
5 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 5 | symgtopn 17648 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) =
(TopOpen‘𝐺)) |
7 | | distopon 20611 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) |
8 | | eqid 2610 |
. . . . . . . 8
⊢
(∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴})) |
9 | 8 | pttoponconst 21210 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚
𝐴))) |
10 | 7, 9 | mpdan 699 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚
𝐴))) |
11 | 1, 5 | elsymgbas 17625 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
12 | | f1of 6050 |
. . . . . . . . 9
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴) |
13 | | elmapg 7757 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (𝐴 ↑𝑚 𝐴) ↔ 𝑥:𝐴⟶𝐴)) |
14 | 13 | anidms 675 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝐴 ↑𝑚 𝐴) ↔ 𝑥:𝐴⟶𝐴)) |
15 | 12, 14 | syl5ibr 235 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1-onto→𝐴 → 𝑥 ∈ (𝐴 ↑𝑚 𝐴))) |
16 | 11, 15 | sylbid 229 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (𝐴 ↑𝑚 𝐴))) |
17 | 16 | ssrdv 3574 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝐴 ↑𝑚 𝐴)) |
18 | | resttopon 20775 |
. . . . . 6
⊢
(((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)) ∧ (Base‘𝐺) ⊆ (𝐴 ↑𝑚 𝐴)) →
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) ∈
(TopOn‘(Base‘𝐺))) |
19 | 10, 17, 18 | syl2anc 691 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) ∈
(TopOn‘(Base‘𝐺))) |
20 | 6, 19 | eqeltrrd 2689 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺))) |
21 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
22 | 5, 21 | istps 20551 |
. . . 4
⊢ (𝐺 ∈ TopSp ↔
(TopOpen‘𝐺) ∈
(TopOn‘(Base‘𝐺))) |
23 | 20, 22 | sylibr 223 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopSp) |
24 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
25 | 1, 5, 24 | symgplusg 17632 |
. . . . . . 7
⊢
(+g‘𝐺) = (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 ∘ 𝑦)) |
26 | | eqid 2610 |
. . . . . . . 8
⊢
((𝒫 𝐴
^ko 𝒫 𝐴) ↾t (Base‘𝐺)) = ((𝒫 𝐴 ^ko 𝒫
𝐴) ↾t
(Base‘𝐺)) |
27 | | distop 20610 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
28 | | eqid 2610 |
. . . . . . . . . 10
⊢
(𝒫 𝐴
^ko 𝒫 𝐴) = (𝒫 𝐴 ^ko 𝒫 𝐴) |
29 | 28 | xkotopon 21213 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ Top) → (𝒫 𝐴 ^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) |
30 | 27, 27, 29 | syl2anc 691 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) |
31 | | cndis 20905 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑𝑚 𝐴)) |
32 | 7, 31 | mpdan 699 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑𝑚 𝐴)) |
33 | 17, 32 | sseqtr4d 3605 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) |
34 | | disllycmp 21111 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Locally Comp) |
35 | | llynlly 21090 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∈
Locally Comp → 𝒫 𝐴 ∈ 𝑛-Locally
Comp) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ 𝑛-Locally
Comp) |
37 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) |
38 | 37 | xkococn 21273 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ 𝑛-Locally Comp ∧ 𝒫 𝐴 ∈ Top) → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ^ko 𝒫 𝐴) ×t (𝒫
𝐴 ^ko
𝒫 𝐴)) Cn (𝒫
𝐴 ^ko
𝒫 𝐴))) |
39 | 27, 36, 27, 38 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ^ko 𝒫 𝐴) ×t (𝒫
𝐴 ^ko
𝒫 𝐴)) Cn (𝒫
𝐴 ^ko
𝒫 𝐴))) |
40 | 26, 30, 33, 26, 30, 33, 39 | cnmpt2res 21290 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺), 𝑦 ∈ (Base‘𝐺) ↦ (𝑥 ∘ 𝑦)) ∈ ((((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))) Cn
(𝒫 𝐴
^ko 𝒫 𝐴))) |
41 | 25, 40 | syl5eqel 2692 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ ((((𝒫 𝐴 ^ko 𝒫
𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))) Cn
(𝒫 𝐴
^ko 𝒫 𝐴))) |
42 | | xkopt 21268 |
. . . . . . . . . . 11
⊢
((𝒫 𝐴 ∈
Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 ^ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) |
43 | 27, 42 | mpancom 700 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ^ko 𝒫 𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) |
44 | 43 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺))) |
45 | 44, 6 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺)) =
(TopOpen‘𝐺)) |
46 | 45, 45 | oveq12d 6567 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))) =
((TopOpen‘𝐺)
×t (TopOpen‘𝐺))) |
47 | 46 | oveq1d 6564 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ((((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))
×t ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))) Cn
(𝒫 𝐴
^ko 𝒫 𝐴)) = (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn (𝒫 𝐴 ^ko 𝒫
𝐴))) |
48 | 41, 47 | eleqtrd 2690 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(𝒫 𝐴
^ko 𝒫 𝐴))) |
49 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
50 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
51 | 49, 50 | coex 7011 |
. . . . . . . . . . 11
⊢ (𝑥 ∘ 𝑦) ∈ V |
52 | 25, 51 | fnmpt2i 7128 |
. . . . . . . . . 10
⊢
(+g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) |
53 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+𝑓‘𝐺) = (+𝑓‘𝐺) |
54 | 5, 24, 53 | plusfeq 17072 |
. . . . . . . . . 10
⊢
((+g‘𝐺) Fn ((Base‘𝐺) × (Base‘𝐺)) → (+𝑓‘𝐺) = (+g‘𝐺)) |
55 | 52, 54 | ax-mp 5 |
. . . . . . . . 9
⊢
(+𝑓‘𝐺) = (+g‘𝐺) |
56 | 55 | eqcomi 2619 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+𝑓‘𝐺) |
57 | 5, 56 | grpplusf 17257 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
(+g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺)) |
58 | | frn 5966 |
. . . . . . 7
⊢
((+g‘𝐺):((Base‘𝐺) × (Base‘𝐺))⟶(Base‘𝐺) → ran (+g‘𝐺) ⊆ (Base‘𝐺)) |
59 | 2, 57, 58 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ran (+g‘𝐺) ⊆ (Base‘𝐺)) |
60 | | cnrest2 20900 |
. . . . . 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 1318 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(𝒫 𝐴
^ko 𝒫 𝐴)) ↔ (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
((𝒫 𝐴
^ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
62 | 48, 61 | mpbid 221 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
((𝒫 𝐴
^ko 𝒫 𝐴) ↾t (Base‘𝐺)))) |
63 | 45 | oveq2d 6565 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (((TopOpen‘𝐺) ×t (TopOpen‘𝐺)) Cn ((𝒫 𝐴 ^ko 𝒫
𝐴) ↾t
(Base‘𝐺))) =
(((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺))) |
64 | 62, 63 | eleqtrd 2690 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) ∈ (((TopOpen‘𝐺) ×t
(TopOpen‘𝐺)) Cn
(TopOpen‘𝐺))) |
65 | 56, 21 | istmd 21688 |
. . 3
⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧
(+g‘𝐺)
∈ (((TopOpen‘𝐺)
×t (TopOpen‘𝐺)) Cn (TopOpen‘𝐺)))) |
66 | 4, 23, 64, 65 | syl3anbrc 1239 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopMnd) |
67 | | id 22 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
68 | | fconst6g 6007 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Top → (𝐴 ×
{𝒫 𝐴}):𝐴⟶Top) |
69 | 27, 68 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 × {𝒫 𝐴}):𝐴⟶Top) |
70 | 11 | biimpa 500 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) |
71 | | f1ocnv 6062 |
. . . . . . . . . . . 12
⊢ (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴) |
72 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (◡𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴⟶𝐴) |
73 | 70, 71, 72 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥:𝐴⟶𝐴) |
74 | 73 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑦 ∈ 𝐴) → (◡𝑥‘𝑦) ∈ 𝐴) |
75 | 74 | an32s 842 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥‘𝑦) ∈ 𝐴) |
76 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) |
77 | 75, 76 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴) |
78 | 77 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴) |
79 | | cnveq 5218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑓 → ◡𝑥 = ◡𝑓) |
80 | 79 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑓 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦)) |
81 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑓‘𝑦) ∈ V |
82 | 80, 76, 81 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦)) |
83 | 82 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦)) |
84 | 83 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡)) |
85 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) |
86 | 85 | mptiniseg 5546 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ V → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) |
87 | 50, 86 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} |
88 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) |
89 | 10 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚
𝐴))) |
90 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (Base‘𝐺) ⊆ (𝐴 ↑𝑚 𝐴)) |
91 | | toponuni 20542 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑𝑚 𝐴)) → (𝐴 ↑𝑚 𝐴) = ∪
(∏t‘(𝐴 × {𝒫 𝐴}))) |
92 | | mpteq1 4665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ↑𝑚
𝐴) = ∪ (∏t‘(𝐴 × {𝒫 𝐴})) → (𝑢 ∈ (𝐴 ↑𝑚 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦)))) |
93 | 89, 91, 92 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑𝑚 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦)))) |
94 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝐴 ∈ 𝑉) |
95 | 69 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝐴 × {𝒫 𝐴}):𝐴⟶Top) |
96 | 1, 5 | elsymgbas 17625 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ 𝑉 → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴)) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴)) |
98 | 97 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓:𝐴–1-1-onto→𝐴) |
99 | | f1ocnv 6062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→𝐴) |
100 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴⟶𝐴) |
101 | 98, 99, 100 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ◡𝑓:𝐴⟶𝐴) |
102 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑦 ∈ 𝐴) |
103 | 101, 102 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴) |
104 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) = ∪
(∏t‘(𝐴 × {𝒫 𝐴})) |
105 | 104, 8 | ptpjcn 21224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝒫 𝐴}):𝐴⟶Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)))) |
106 | 94, 95, 103, 105 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)))) |
107 | 27 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ Top) |
108 | | fvconst2g 6372 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((𝒫 𝐴 ∈
Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴) |
109 | 107, 103,
108 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴) |
110 | 109 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦))) = ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) |
111 | 106, 110 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) |
112 | 93, 111 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑𝑚 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) |
113 | 88, 89, 90, 112 | cnmpt1res 21289 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴)) |
114 | 6 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ 𝑉 → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴) =
((TopOpen‘𝐺) Cn
𝒫 𝐴)) |
115 | 114 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴) =
((TopOpen‘𝐺) Cn
𝒫 𝐴)) |
116 | 113, 115 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴)) |
117 | | snelpwi 4839 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) |
118 | 117 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑦} ∈ 𝒫 𝐴) |
119 | | cnima 20879 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ∧ {𝑦} ∈ 𝒫 𝐴) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺)) |
120 | 116, 118,
119 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺)) |
121 | 87, 120 | syl5eqelr 2693 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺)) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺)) |
123 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ (Base‘𝐺)) |
124 | 98 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓:𝐴–1-1-onto→𝐴) |
125 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑦 ∈ 𝐴) |
126 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦) |
127 | 124, 125,
126 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦) |
128 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑓 → (𝑢‘(◡𝑓‘𝑦)) = (𝑓‘(◡𝑓‘𝑦))) |
129 | 128 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑓 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑓‘(◡𝑓‘𝑦)) = 𝑦)) |
130 | 129 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ↔ (𝑓 ∈ (Base‘𝐺) ∧ (𝑓‘(◡𝑓‘𝑦)) = 𝑦)) |
131 | 123, 127,
130 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) |
132 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺)) |
134 | 11 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
135 | 134 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) |
136 | 103 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴) |
137 | | f1ocnvfv 6434 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥:𝐴–1-1-onto→𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))) |
138 | 135, 136,
137 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))) |
139 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝑡) |
140 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → ((◡𝑥‘𝑦) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡)) |
141 | 139, 140 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → (◡𝑥‘𝑦) ∈ 𝑡)) |
142 | 138, 141 | syld 46 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) |
143 | 142 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) |
144 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑥 → (𝑢‘(◡𝑓‘𝑦)) = (𝑥‘(◡𝑓‘𝑦))) |
145 | 144 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑥 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑥‘(◡𝑓‘𝑦)) = 𝑦)) |
146 | 145 | ralrab 3335 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
{𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) |
147 | 143, 146 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡) |
148 | | ssrab 3643 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} ↔ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) ∧ ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡)) |
149 | 133, 147,
148 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡}) |
150 | 76 | mptpreima 5545 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡) = {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} |
151 | 149, 150 | syl6sseqr 3615 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡)) |
152 | | funmpt 5840 |
. . . . . . . . . . . . . . . 16
⊢ Fun
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) |
153 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝑥‘𝑦) ∈ V |
154 | 153, 76 | dmmpti 5936 |
. . . . . . . . . . . . . . . . 17
⊢ dom
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (Base‘𝐺) |
155 | 133, 154 | syl6sseqr 3615 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) |
156 | | funimass3 6241 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∧ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))) |
157 | 152, 155,
156 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))) |
158 | 151, 157 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡) |
159 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (𝑓 ∈ 𝑣 ↔ 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})) |
160 | | imaeq2 5381 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) = ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})) |
161 | 160 | sseq1d 3595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡 ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) |
162 | 159, 161 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡) ↔ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡))) |
163 | 162 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺) ∧ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)) |
164 | 122, 131,
158, 163 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)) |
165 | 164 | expr 641 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((◡𝑓‘𝑦) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) |
166 | 84, 165 | sylbid 229 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) |
167 | 166 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) |
168 | 20 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺))) |
169 | 7 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ (TopOn‘𝐴)) |
170 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓 ∈ (Base‘𝐺)) |
171 | | iscnp 20851 |
. . . . . . . . . . 11
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))))) |
172 | 168, 169,
170, 171 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))))) |
173 | 78, 167, 172 | mpbir2and 959 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)) |
174 | 173 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)) |
175 | | cncnp 20894 |
. . . . . . . . . 10
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) |
176 | 20, 7, 175 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) |
177 | 176 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) |
178 | 77, 174, 177 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴)) |
179 | | fvconst2g 6372 |
. . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴) |
180 | 27, 179 | sylan 487 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴) |
181 | 180 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)) = ((TopOpen‘𝐺) Cn 𝒫 𝐴)) |
182 | 178, 181 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦))) |
183 | 8, 20, 67, 69, 182 | ptcn 21240 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) ∈ ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴})))) |
184 | | eqid 2610 |
. . . . . . . . 9
⊢
(invg‘𝐺) = (invg‘𝐺) |
185 | 5, 184 | grpinvf 17289 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
186 | 2, 185 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) |
187 | 186 | feqmptd 6159 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥))) |
188 | 1, 5, 184 | symginv 17645 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝐺) →
((invg‘𝐺)‘𝑥) = ◡𝑥) |
189 | 188 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = ◡𝑥) |
190 | 73 | feqmptd 6159 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥 = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) |
191 | 189, 190 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) |
192 | 191 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))) |
193 | 187, 192 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))) |
194 | 43 | oveq2d 6565 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫 𝐴)) = ((TopOpen‘𝐺) Cn
(∏t‘(𝐴 × {𝒫 𝐴})))) |
195 | 183, 193,
194 | 3eltr4d 2703 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫
𝐴))) |
196 | | frn 5966 |
. . . . . 6
⊢
((invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺) → ran (invg‘𝐺) ⊆ (Base‘𝐺)) |
197 | 2, 185, 196 | 3syl 18 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → ran (invg‘𝐺) ⊆ (Base‘𝐺)) |
198 | | cnrest2 20900 |
. . . . 5
⊢
(((𝒫 𝐴
^ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (invg‘𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫
𝐴)) ↔
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn ((𝒫 𝐴
^ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
199 | 30, 197, 33, 198 | syl3anc 1318 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ^ko 𝒫
𝐴)) ↔
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn ((𝒫 𝐴
^ko 𝒫 𝐴) ↾t (Base‘𝐺))))) |
200 | 195, 199 | mpbid 221 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ^ko 𝒫
𝐴) ↾t
(Base‘𝐺)))) |
201 | 45 | oveq2d 6565 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ^ko 𝒫 𝐴) ↾t
(Base‘𝐺))) =
((TopOpen‘𝐺) Cn
(TopOpen‘𝐺))) |
202 | 200, 201 | eleqtrd 2690 |
. 2
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))) |
203 | 21, 184 | istgp 21691 |
. 2
⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺)))) |
204 | 2, 66, 202, 203 | syl3anbrc 1239 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp) |