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

Theorem symgtgp 23457
Description: The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof shortened by AV, 30-Mar-2024.)
Hypothesis
Ref Expression
symgtgp.g 𝐺 = (SymGrp‘𝐴)
Assertion
Ref Expression
symgtgp (𝐴𝑉𝐺 ∈ TopGrp)

Proof of Theorem symgtgp
Dummy variables 𝑡 𝑓 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 symgtgp.g . . 3 𝐺 = (SymGrp‘𝐴)
21symggrp 19182 . 2 (𝐴𝑉𝐺 ∈ Grp)
3 eqid 2736 . . . 4 (EndoFMnd‘𝐴) = (EndoFMnd‘𝐴)
43efmndtmd 23452 . . 3 (𝐴𝑉 → (EndoFMnd‘𝐴) ∈ TopMnd)
5 eqid 2736 . . . 4 (Base‘𝐺) = (Base‘𝐺)
63, 1, 5symgsubmefmnd 19180 . . 3 (𝐴𝑉 → (Base‘𝐺) ∈ (SubMnd‘(EndoFMnd‘𝐴)))
71, 5, 3symgressbas 19163 . . . 4 𝐺 = ((EndoFMnd‘𝐴) ↾s (Base‘𝐺))
87submtmd 23455 . . 3 (((EndoFMnd‘𝐴) ∈ TopMnd ∧ (Base‘𝐺) ∈ (SubMnd‘(EndoFMnd‘𝐴))) → 𝐺 ∈ TopMnd)
94, 6, 8syl2anc 584 . 2 (𝐴𝑉𝐺 ∈ TopMnd)
10 eqid 2736 . . . . . 6 (∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴}))
111, 5symgtopn 19188 . . . . . . 7 (𝐴𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) = (TopOpen‘𝐺))
12 distopon 22347 . . . . . . . . 9 (𝐴𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
1310pttoponconst 22948 . . . . . . . . 9 ((𝐴𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴m 𝐴)))
1412, 13mpdan 685 . . . . . . . 8 (𝐴𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴m 𝐴)))
151, 5elsymgbas 19155 . . . . . . . . . 10 (𝐴𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴1-1-onto𝐴))
16 f1of 6784 . . . . . . . . . . 11 (𝑥:𝐴1-1-onto𝐴𝑥:𝐴𝐴)
17 elmapg 8778 . . . . . . . . . . . 12 ((𝐴𝑉𝐴𝑉) → (𝑥 ∈ (𝐴m 𝐴) ↔ 𝑥:𝐴𝐴))
1817anidms 567 . . . . . . . . . . 11 (𝐴𝑉 → (𝑥 ∈ (𝐴m 𝐴) ↔ 𝑥:𝐴𝐴))
1916, 18syl5ibr 245 . . . . . . . . . 10 (𝐴𝑉 → (𝑥:𝐴1-1-onto𝐴𝑥 ∈ (𝐴m 𝐴)))
2015, 19sylbid 239 . . . . . . . . 9 (𝐴𝑉 → (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (𝐴m 𝐴)))
2120ssrdv 3950 . . . . . . . 8 (𝐴𝑉 → (Base‘𝐺) ⊆ (𝐴m 𝐴))
22 resttopon 22512 . . . . . . . 8 (((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴m 𝐴)) ∧ (Base‘𝐺) ⊆ (𝐴m 𝐴)) → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) ∈ (TopOn‘(Base‘𝐺)))
2314, 21, 22syl2anc 584 . . . . . . 7 (𝐴𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) ∈ (TopOn‘(Base‘𝐺)))
2411, 23eqeltrrd 2839 . . . . . 6 (𝐴𝑉 → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)))
25 id 22 . . . . . 6 (𝐴𝑉𝐴𝑉)
26 distop 22345 . . . . . . 7 (𝐴𝑉 → 𝒫 𝐴 ∈ Top)
27 fconst6g 6731 . . . . . . 7 (𝒫 𝐴 ∈ Top → (𝐴 × {𝒫 𝐴}):𝐴⟶Top)
2826, 27syl 17 . . . . . 6 (𝐴𝑉 → (𝐴 × {𝒫 𝐴}):𝐴⟶Top)
2915biimpa 477 . . . . . . . . . . . 12 ((𝐴𝑉𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴1-1-onto𝐴)
30 f1ocnv 6796 . . . . . . . . . . . 12 (𝑥:𝐴1-1-onto𝐴𝑥:𝐴1-1-onto𝐴)
31 f1of 6784 . . . . . . . . . . . 12 (𝑥:𝐴1-1-onto𝐴𝑥:𝐴𝐴)
3229, 30, 313syl 18 . . . . . . . . . . 11 ((𝐴𝑉𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴𝐴)
3332ffvelcdmda 7035 . . . . . . . . . 10 (((𝐴𝑉𝑥 ∈ (Base‘𝐺)) ∧ 𝑦𝐴) → (𝑥𝑦) ∈ 𝐴)
3433an32s 650 . . . . . . . . 9 (((𝐴𝑉𝑦𝐴) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑥𝑦) ∈ 𝐴)
3534fmpttd 7063 . . . . . . . 8 ((𝐴𝑉𝑦𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴)
3635adantr 481 . . . . . . . . . 10 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴)
37 cnveq 5829 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑓𝑥 = 𝑓)
3837fveq1d 6844 . . . . . . . . . . . . . . 15 (𝑥 = 𝑓 → (𝑥𝑦) = (𝑓𝑦))
39 eqid 2736 . . . . . . . . . . . . . . 15 (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))
40 fvex 6855 . . . . . . . . . . . . . . 15 (𝑓𝑦) ∈ V
4138, 39, 40fvmpt 6948 . . . . . . . . . . . . . 14 (𝑓 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) = (𝑓𝑦))
4241ad2antlr 725 . . . . . . . . . . . . 13 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) = (𝑓𝑦))
4342eleq1d 2822 . . . . . . . . . . . 12 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) ∈ 𝑡 ↔ (𝑓𝑦) ∈ 𝑡))
44 eqid 2736 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) = (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦)))
4544mptiniseg 6191 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ V → ((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦})
4645elv 3451 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}
47 eqid 2736 . . . . . . . . . . . . . . . . . . 19 ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) = ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺))
4814ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴m 𝐴)))
4921ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (Base‘𝐺) ⊆ (𝐴m 𝐴))
50 toponuni 22263 . . . . . . . . . . . . . . . . . . . . 21 ((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴m 𝐴)) → (𝐴m 𝐴) = (∏t‘(𝐴 × {𝒫 𝐴})))
51 mpteq1 5198 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴m 𝐴) = (∏t‘(𝐴 × {𝒫 𝐴})) → (𝑢 ∈ (𝐴m 𝐴) ↦ (𝑢‘(𝑓𝑦))) = (𝑢 (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(𝑓𝑦))))
5248, 50, 513syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴m 𝐴) ↦ (𝑢‘(𝑓𝑦))) = (𝑢 (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(𝑓𝑦))))
53 simpll 765 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝐴𝑉)
5428ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝐴 × {𝒫 𝐴}):𝐴⟶Top)
551, 5elsymgbas 19155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴𝑉 → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴1-1-onto𝐴))
5655adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴𝑉𝑦𝐴) → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴1-1-onto𝐴))
5756biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓:𝐴1-1-onto𝐴)
58 f1ocnv 6796 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝐴1-1-onto𝐴𝑓:𝐴1-1-onto𝐴)
59 f1of 6784 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓:𝐴1-1-onto𝐴𝑓:𝐴𝐴)
6057, 58, 593syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓:𝐴𝐴)
61 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑦𝐴)
6260, 61ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑓𝑦) ∈ 𝐴)
63 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴}))
6463, 10ptpjcn 22962 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉 ∧ (𝐴 × {𝒫 𝐴}):𝐴⟶Top ∧ (𝑓𝑦) ∈ 𝐴) → (𝑢 (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(𝑓𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(𝑓𝑦))))
6553, 54, 62, 64syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(𝑓𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(𝑓𝑦))))
6626ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ Top)
67 fvconst2g 7151 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝒫 𝐴 ∈ Top ∧ (𝑓𝑦) ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘(𝑓𝑦)) = 𝒫 𝐴)
6866, 62, 67syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝐴 × {𝒫 𝐴})‘(𝑓𝑦)) = 𝒫 𝐴)
6968oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(𝑓𝑦))) = ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴))
7065, 69eleqtrd 2840 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 (∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(𝑓𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴))
7152, 70eqeltrd 2838 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴m 𝐴) ↦ (𝑢‘(𝑓𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴))
7247, 48, 49, 71cnmpt1res 23027 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) ∈ (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) Cn 𝒫 𝐴))
7311oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝐴𝑉 → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) Cn 𝒫 𝐴) = ((TopOpen‘𝐺) Cn 𝒫 𝐴))
7473ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) Cn 𝒫 𝐴) = ((TopOpen‘𝐺) Cn 𝒫 𝐴))
7572, 74eleqtrd 2840 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴))
76 snelpwi 5400 . . . . . . . . . . . . . . . . . 18 (𝑦𝐴 → {𝑦} ∈ 𝒫 𝐴)
7776ad2antlr 725 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑦} ∈ 𝒫 𝐴)
78 cnima 22616 . . . . . . . . . . . . . . . . 17 (((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ∧ {𝑦} ∈ 𝒫 𝐴) → ((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺))
7975, 77, 78syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(𝑓𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺))
8046, 79eqeltrrid 2843 . . . . . . . . . . . . . . 15 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ∈ (TopOpen‘𝐺))
8180adantr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ∈ (TopOpen‘𝐺))
82 fveq1 6841 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑓 → (𝑢‘(𝑓𝑦)) = (𝑓‘(𝑓𝑦)))
8382eqeq1d 2738 . . . . . . . . . . . . . . 15 (𝑢 = 𝑓 → ((𝑢‘(𝑓𝑦)) = 𝑦 ↔ (𝑓‘(𝑓𝑦)) = 𝑦))
84 simplr 767 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → 𝑓 ∈ (Base‘𝐺))
8557adantr 481 . . . . . . . . . . . . . . . 16 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → 𝑓:𝐴1-1-onto𝐴)
86 simpllr 774 . . . . . . . . . . . . . . . 16 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → 𝑦𝐴)
87 f1ocnvfv2 7223 . . . . . . . . . . . . . . . 16 ((𝑓:𝐴1-1-onto𝐴𝑦𝐴) → (𝑓‘(𝑓𝑦)) = 𝑦)
8885, 86, 87syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → (𝑓‘(𝑓𝑦)) = 𝑦)
8983, 84, 88elrabd 3647 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦})
90 ssrab2 4037 . . . . . . . . . . . . . . . . . 18 {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ (Base‘𝐺)
9190a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ (Base‘𝐺))
9215ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴1-1-onto𝐴))
9392biimpa 477 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴1-1-onto𝐴)
9462ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑓𝑦) ∈ 𝐴)
95 f1ocnvfv 7224 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥:𝐴1-1-onto𝐴 ∧ (𝑓𝑦) ∈ 𝐴) → ((𝑥‘(𝑓𝑦)) = 𝑦 → (𝑥𝑦) = (𝑓𝑦)))
9693, 94, 95syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(𝑓𝑦)) = 𝑦 → (𝑥𝑦) = (𝑓𝑦)))
97 simplrr 776 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑓𝑦) ∈ 𝑡)
98 eleq1 2825 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝑦) = (𝑓𝑦) → ((𝑥𝑦) ∈ 𝑡 ↔ (𝑓𝑦) ∈ 𝑡))
9997, 98syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥𝑦) = (𝑓𝑦) → (𝑥𝑦) ∈ 𝑡))
10096, 99syld 47 . . . . . . . . . . . . . . . . . . 19 (((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(𝑓𝑦)) = 𝑦 → (𝑥𝑦) ∈ 𝑡))
101100ralrimiva 3143 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(𝑓𝑦)) = 𝑦 → (𝑥𝑦) ∈ 𝑡))
102 fveq1 6841 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑢‘(𝑓𝑦)) = (𝑥‘(𝑓𝑦)))
103102eqeq1d 2738 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑢‘(𝑓𝑦)) = 𝑦 ↔ (𝑥‘(𝑓𝑦)) = 𝑦))
104103ralrab 3651 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} (𝑥𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(𝑓𝑦)) = 𝑦 → (𝑥𝑦) ∈ 𝑡))
105101, 104sylibr 233 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} (𝑥𝑦) ∈ 𝑡)
106 ssrab 4030 . . . . . . . . . . . . . . . . 17 ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (𝑥𝑦) ∈ 𝑡} ↔ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ (Base‘𝐺) ∧ ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} (𝑥𝑦) ∈ 𝑡))
10791, 105, 106sylanbrc 583 . . . . . . . . . . . . . . . 16 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (𝑥𝑦) ∈ 𝑡})
10839mptpreima 6190 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑡) = {𝑥 ∈ (Base‘𝐺) ∣ (𝑥𝑦) ∈ 𝑡}
109107, 108sseqtrrdi 3995 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑡))
110 funmpt 6539 . . . . . . . . . . . . . . . 16 Fun (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))
111 fvex 6855 . . . . . . . . . . . . . . . . . 18 (𝑥𝑦) ∈ V
112111, 39dmmpti 6645 . . . . . . . . . . . . . . . . 17 dom (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) = (Base‘𝐺)
11391, 112sseqtrrdi 3995 . . . . . . . . . . . . . . . 16 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)))
114 funimass3 7004 . . . . . . . . . . . . . . . 16 ((Fun (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∧ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))) → (((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑡)))
115110, 113, 114sylancr 587 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → (((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ⊆ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑡)))
116109, 115mpbird 256 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}) ⊆ 𝑡)
117 eleq2 2826 . . . . . . . . . . . . . . . 16 (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} → (𝑓𝑣𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}))
118 imaeq2 6009 . . . . . . . . . . . . . . . . 17 (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) = ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}))
119118sseq1d 3975 . . . . . . . . . . . . . . . 16 (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} → (((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡 ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}) ⊆ 𝑡))
120117, 119anbi12d 631 . . . . . . . . . . . . . . 15 (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} → ((𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡) ↔ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}) ⊆ 𝑡)))
121120rspcev 3581 . . . . . . . . . . . . . 14 (({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ∈ (TopOpen‘𝐺) ∧ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(𝑓𝑦)) = 𝑦}) ⊆ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡))
12281, 89, 116, 121syl12anc 835 . . . . . . . . . . . . 13 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (𝑓𝑦) ∈ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡))
123122expr 457 . . . . . . . . . . . 12 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((𝑓𝑦) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡)))
12443, 123sylbid 239 . . . . . . . . . . 11 ((((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡)))
125124ralrimiva 3143 . . . . . . . . . 10 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡)))
12624ad2antrr 724 . . . . . . . . . . 11 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)))
12712ad2antrr 724 . . . . . . . . . . 11 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ (TopOn‘𝐴))
128 simpr 485 . . . . . . . . . . 11 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓 ∈ (Base‘𝐺))
129 iscnp 22588 . . . . . . . . . . 11 (((TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡)))))
130126, 127, 128, 129syl3anc 1371 . . . . . . . . . 10 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) “ 𝑣) ⊆ 𝑡)))))
13136, 125, 130mpbir2and 711 . . . . . . . . 9 (((𝐴𝑉𝑦𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))
132131ralrimiva 3143 . . . . . . . 8 ((𝐴𝑉𝑦𝐴) → ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))
133 cncnp 22631 . . . . . . . . . 10 (((TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))))
13424, 12, 133syl2anc 584 . . . . . . . . 9 (𝐴𝑉 → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))))
135134adantr 481 . . . . . . . 8 ((𝐴𝑉𝑦𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓))))
13635, 132, 135mpbir2and 711 . . . . . . 7 ((𝐴𝑉𝑦𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴))
137 fvconst2g 7151 . . . . . . . . 9 ((𝒫 𝐴 ∈ Top ∧ 𝑦𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴)
13826, 137sylan 580 . . . . . . . 8 ((𝐴𝑉𝑦𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴)
139138oveq2d 7373 . . . . . . 7 ((𝐴𝑉𝑦𝐴) → ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)) = ((TopOpen‘𝐺) Cn 𝒫 𝐴))
140136, 139eleqtrrd 2841 . . . . . 6 ((𝐴𝑉𝑦𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (𝑥𝑦)) ∈ ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)))
14110, 24, 25, 28, 140ptcn 22978 . . . . 5 (𝐴𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ (𝑦𝐴 ↦ (𝑥𝑦))) ∈ ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴}))))
142 eqid 2736 . . . . . . . . 9 (invg𝐺) = (invg𝐺)
1435, 142grpinvf 18797 . . . . . . . 8 (𝐺 ∈ Grp → (invg𝐺):(Base‘𝐺)⟶(Base‘𝐺))
1442, 143syl 17 . . . . . . 7 (𝐴𝑉 → (invg𝐺):(Base‘𝐺)⟶(Base‘𝐺))
145144feqmptd 6910 . . . . . 6 (𝐴𝑉 → (invg𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((invg𝐺)‘𝑥)))
1461, 5, 142symginv 19184 . . . . . . . . 9 (𝑥 ∈ (Base‘𝐺) → ((invg𝐺)‘𝑥) = 𝑥)
147146adantl 482 . . . . . . . 8 ((𝐴𝑉𝑥 ∈ (Base‘𝐺)) → ((invg𝐺)‘𝑥) = 𝑥)
14832feqmptd 6910 . . . . . . . 8 ((𝐴𝑉𝑥 ∈ (Base‘𝐺)) → 𝑥 = (𝑦𝐴 ↦ (𝑥𝑦)))
149147, 148eqtrd 2776 . . . . . . 7 ((𝐴𝑉𝑥 ∈ (Base‘𝐺)) → ((invg𝐺)‘𝑥) = (𝑦𝐴 ↦ (𝑥𝑦)))
150149mpteq2dva 5205 . . . . . 6 (𝐴𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ ((invg𝐺)‘𝑥)) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦𝐴 ↦ (𝑥𝑦))))
151145, 150eqtrd 2776 . . . . 5 (𝐴𝑉 → (invg𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦𝐴 ↦ (𝑥𝑦))))
152 xkopt 23006 . . . . . . 7 ((𝒫 𝐴 ∈ Top ∧ 𝐴𝑉) → (𝒫 𝐴ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝒫 𝐴})))
15326, 152mpancom 686 . . . . . 6 (𝐴𝑉 → (𝒫 𝐴ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝒫 𝐴})))
154153oveq2d 7373 . . . . 5 (𝐴𝑉 → ((TopOpen‘𝐺) Cn (𝒫 𝐴ko 𝒫 𝐴)) = ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴}))))
155141, 151, 1543eltr4d 2853 . . . 4 (𝐴𝑉 → (invg𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴ko 𝒫 𝐴)))
156 eqid 2736 . . . . . . 7 (𝒫 𝐴ko 𝒫 𝐴) = (𝒫 𝐴ko 𝒫 𝐴)
157156xkotopon 22951 . . . . . 6 ((𝒫 𝐴 ∈ Top ∧ 𝒫 𝐴 ∈ Top) → (𝒫 𝐴ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)))
15826, 26, 157syl2anc 584 . . . . 5 (𝐴𝑉 → (𝒫 𝐴ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)))
159 frn 6675 . . . . . 6 ((invg𝐺):(Base‘𝐺)⟶(Base‘𝐺) → ran (invg𝐺) ⊆ (Base‘𝐺))
1602, 143, 1593syl 18 . . . . 5 (𝐴𝑉 → ran (invg𝐺) ⊆ (Base‘𝐺))
161 cndis 22642 . . . . . . 7 ((𝐴𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴m 𝐴))
16212, 161mpdan 685 . . . . . 6 (𝐴𝑉 → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴m 𝐴))
16321, 162sseqtrrd 3985 . . . . 5 (𝐴𝑉 → (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴))
164 cnrest2 22637 . . . . 5 (((𝒫 𝐴ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (invg𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((invg𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴ko 𝒫 𝐴)) ↔ (invg𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴ko 𝒫 𝐴) ↾t (Base‘𝐺)))))
165158, 160, 163, 164syl3anc 1371 . . . 4 (𝐴𝑉 → ((invg𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴ko 𝒫 𝐴)) ↔ (invg𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴ko 𝒫 𝐴) ↾t (Base‘𝐺)))))
166155, 165mpbid 231 . . 3 (𝐴𝑉 → (invg𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴ko 𝒫 𝐴) ↾t (Base‘𝐺))))
167153oveq1d 7372 . . . . 5 (𝐴𝑉 → ((𝒫 𝐴ko 𝒫 𝐴) ↾t (Base‘𝐺)) = ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)))
168167, 11eqtrd 2776 . . . 4 (𝐴𝑉 → ((𝒫 𝐴ko 𝒫 𝐴) ↾t (Base‘𝐺)) = (TopOpen‘𝐺))
169168oveq2d 7373 . . 3 (𝐴𝑉 → ((TopOpen‘𝐺) Cn ((𝒫 𝐴ko 𝒫 𝐴) ↾t (Base‘𝐺))) = ((TopOpen‘𝐺) Cn (TopOpen‘𝐺)))
170166, 169eleqtrd 2840 . 2 (𝐴𝑉 → (invg𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺)))
171 eqid 2736 . . 3 (TopOpen‘𝐺) = (TopOpen‘𝐺)
172171, 142istgp 23428 . 2 (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ (invg𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))))
1732, 9, 170, 172syl3anbrc 1343 1 (𝐴𝑉𝐺 ∈ TopGrp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  wss 3910  𝒫 cpw 4560  {csn 4586   cuni 4865  cmpt 5188   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cima 5636  Fun wfun 6490  wf 6492  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  m cmap 8765  Basecbs 17083  t crest 17302  TopOpenctopn 17303  tcpt 17320  SubMndcsubmnd 18600  EndoFMndcefmnd 18678  Grpcgrp 18748  invgcminusg 18749  SymGrpcsymg 19148  Topctop 22242  TopOnctopon 22259   Cn ccn 22575   CnP ccnp 22576  ko cxko 22912  TopMndctmd 23421  TopGrpctgp 23422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-tset 17152  df-rest 17304  df-topn 17305  df-0g 17323  df-topgen 17325  df-pt 17326  df-plusf 18496  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-efmnd 18679  df-grp 18751  df-minusg 18752  df-symg 19149  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-ntr 22371  df-nei 22449  df-cn 22578  df-cnp 22579  df-cmp 22738  df-lly 22817  df-nlly 22818  df-tx 22913  df-xko 22914  df-tmd 23423  df-tgp 23424
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator