| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | symgtgp.g | . . 3
⊢ 𝐺 = (SymGrp‘𝐴) | 
| 2 | 1 | symggrp 19419 | . 2
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp) | 
| 3 |  | eqid 2736 | . . . 4
⊢
(EndoFMnd‘𝐴) =
(EndoFMnd‘𝐴) | 
| 4 | 3 | efmndtmd 24110 | . . 3
⊢ (𝐴 ∈ 𝑉 → (EndoFMnd‘𝐴) ∈ TopMnd) | 
| 5 |  | eqid 2736 | . . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 6 | 3, 1, 5 | symgsubmefmnd 19417 | . . 3
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ∈ (SubMnd‘(EndoFMnd‘𝐴))) | 
| 7 | 1, 5, 3 | symgressbas 19400 | . . . 4
⊢ 𝐺 = ((EndoFMnd‘𝐴) ↾s
(Base‘𝐺)) | 
| 8 | 7 | submtmd 24113 | . . 3
⊢
(((EndoFMnd‘𝐴)
∈ TopMnd ∧ (Base‘𝐺) ∈ (SubMnd‘(EndoFMnd‘𝐴))) → 𝐺 ∈ TopMnd) | 
| 9 | 4, 6, 8 | syl2anc 584 | . 2
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopMnd) | 
| 10 |  | eqid 2736 | . . . . . 6
⊢
(∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴})) | 
| 11 | 1, 5 | symgtopn 19425 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) =
(TopOpen‘𝐺)) | 
| 12 |  | distopon 23005 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | 
| 13 | 10 | pttoponconst 23606 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) | 
| 14 | 12, 13 | mpdan 687 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) | 
| 15 | 1, 5 | elsymgbas 19392 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) | 
| 16 |  | f1of 6847 | . . . . . . . . . . 11
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴) | 
| 17 |  | elmapg 8880 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (𝐴 ↑m 𝐴) ↔ 𝑥:𝐴⟶𝐴)) | 
| 18 | 17 | anidms 566 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝐴 ↑m 𝐴) ↔ 𝑥:𝐴⟶𝐴)) | 
| 19 | 16, 18 | imbitrrid 246 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1-onto→𝐴 → 𝑥 ∈ (𝐴 ↑m 𝐴))) | 
| 20 | 15, 19 | sylbid 240 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) → 𝑥 ∈ (𝐴 ↑m 𝐴))) | 
| 21 | 20 | ssrdv 3988 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝐴 ↑m 𝐴)) | 
| 22 |  | resttopon 23170 | . . . . . . . 8
⊢
(((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴)) ∧ (Base‘𝐺) ⊆ (𝐴 ↑m 𝐴)) → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) ∈
(TopOn‘(Base‘𝐺))) | 
| 23 | 14, 21, 22 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) ∈
(TopOn‘(Base‘𝐺))) | 
| 24 | 11, 23 | eqeltrrd 2841 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺))) | 
| 25 |  | id 22 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) | 
| 26 |  | distop 23003 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) | 
| 27 |  | fconst6g 6796 | . . . . . . 7
⊢
(𝒫 𝐴 ∈
Top → (𝐴 ×
{𝒫 𝐴}):𝐴⟶Top) | 
| 28 | 26, 27 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 × {𝒫 𝐴}):𝐴⟶Top) | 
| 29 | 15 | biimpa 476 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) | 
| 30 |  | f1ocnv 6859 | . . . . . . . . . . . 12
⊢ (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴) | 
| 31 |  | f1of 6847 | . . . . . . . . . . . 12
⊢ (◡𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴⟶𝐴) | 
| 32 | 29, 30, 31 | 3syl 18 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥:𝐴⟶𝐴) | 
| 33 | 32 | ffvelcdmda 7103 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) ∧ 𝑦 ∈ 𝐴) → (◡𝑥‘𝑦) ∈ 𝐴) | 
| 34 | 33 | an32s 652 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥‘𝑦) ∈ 𝐴) | 
| 35 | 34 | fmpttd 7134 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴) | 
| 37 |  | cnveq 5883 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑓 → ◡𝑥 = ◡𝑓) | 
| 38 | 37 | fveq1d 6907 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑓 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦)) | 
| 39 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) | 
| 40 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢ (◡𝑓‘𝑦) ∈ V | 
| 41 | 38, 39, 40 | fvmpt 7015 | . . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (Base‘𝐺) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦)) | 
| 42 | 41 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) = (◡𝑓‘𝑦)) | 
| 43 | 42 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡)) | 
| 44 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) | 
| 45 | 44 | mptiniseg 6258 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ V → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) | 
| 46 | 45 | elv 3484 | . . . . . . . . . . . . . . . 16
⊢ (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} | 
| 47 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺)) | 
| 48 | 14 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) | 
| 49 | 21 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (Base‘𝐺) ⊆ (𝐴 ↑m 𝐴)) | 
| 50 |  | toponuni 22921 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴)) → (𝐴 ↑m 𝐴) = ∪
(∏t‘(𝐴 × {𝒫 𝐴}))) | 
| 51 |  | mpteq1 5234 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ↑m 𝐴) = ∪
(∏t‘(𝐴 × {𝒫 𝐴})) → (𝑢 ∈ (𝐴 ↑m 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦)))) | 
| 52 | 48, 50, 51 | 3syl 18 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑m 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) = (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦)))) | 
| 53 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝐴 ∈ 𝑉) | 
| 54 | 28 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝐴 × {𝒫 𝐴}):𝐴⟶Top) | 
| 55 | 1, 5 | elsymgbas 19392 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ 𝑉 → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴)) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑓 ∈ (Base‘𝐺) ↔ 𝑓:𝐴–1-1-onto→𝐴)) | 
| 57 | 56 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓:𝐴–1-1-onto→𝐴) | 
| 58 |  | f1ocnv 6859 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→𝐴) | 
| 59 |  | f1of 6847 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡𝑓:𝐴–1-1-onto→𝐴 → ◡𝑓:𝐴⟶𝐴) | 
| 60 | 57, 58, 59 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ◡𝑓:𝐴⟶𝐴) | 
| 61 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑦 ∈ 𝐴) | 
| 62 | 60, 61 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴) | 
| 63 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ (∏t‘(𝐴 × {𝒫 𝐴})) = ∪
(∏t‘(𝐴 × {𝒫 𝐴})) | 
| 64 | 63, 10 | ptpjcn 23620 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝒫 𝐴}):𝐴⟶Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)))) | 
| 65 | 53, 54, 62, 64 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)))) | 
| 66 | 26 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ Top) | 
| 67 |  | fvconst2g 7223 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((𝒫 𝐴 ∈
Top ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴) | 
| 68 | 66, 62, 67 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦)) = 𝒫 𝐴) | 
| 69 | 68 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((∏t‘(𝐴 × {𝒫 𝐴})) Cn ((𝐴 × {𝒫 𝐴})‘(◡𝑓‘𝑦))) = ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) | 
| 70 | 65, 69 | eleqtrd 2842 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ ∪
(∏t‘(𝐴 × {𝒫 𝐴})) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) | 
| 71 | 52, 70 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (𝐴 ↑m 𝐴) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((∏t‘(𝐴 × {𝒫 𝐴})) Cn 𝒫 𝐴)) | 
| 72 | 47, 48, 49, 71 | cnmpt1res 23685 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴)) | 
| 73 | 11 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ 𝑉 → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴) =
((TopOpen‘𝐺) Cn
𝒫 𝐴)) | 
| 74 | 73 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝐺)) Cn
𝒫 𝐴) =
((TopOpen‘𝐺) Cn
𝒫 𝐴)) | 
| 75 | 72, 74 | eleqtrd 2842 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴)) | 
| 76 |  | snelpwi 5447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐴 → {𝑦} ∈ 𝒫 𝐴) | 
| 77 | 76 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑦} ∈ 𝒫 𝐴) | 
| 78 |  | cnima 23274 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ∧ {𝑦} ∈ 𝒫 𝐴) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺)) | 
| 79 | 75, 77, 78 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (◡(𝑢 ∈ (Base‘𝐺) ↦ (𝑢‘(◡𝑓‘𝑦))) “ {𝑦}) ∈ (TopOpen‘𝐺)) | 
| 80 | 46, 79 | eqeltrrid 2845 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺)) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺)) | 
| 82 |  | fveq1 6904 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑓 → (𝑢‘(◡𝑓‘𝑦)) = (𝑓‘(◡𝑓‘𝑦))) | 
| 83 | 82 | eqeq1d 2738 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑓 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑓‘(◡𝑓‘𝑦)) = 𝑦)) | 
| 84 |  | simplr 768 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ (Base‘𝐺)) | 
| 85 | 57 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓:𝐴–1-1-onto→𝐴) | 
| 86 |  | simpllr 775 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑦 ∈ 𝐴) | 
| 87 |  | f1ocnvfv2 7298 | . . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦) | 
| 88 | 85, 86, 87 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑓‘(◡𝑓‘𝑦)) = 𝑦) | 
| 89 | 83, 84, 88 | elrabd 3693 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) | 
| 90 |  | ssrab2 4079 | . . . . . . . . . . . . . . . . . 18
⊢ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) | 
| 91 | 90 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺)) | 
| 92 | 15 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) | 
| 93 | 92 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) | 
| 94 | 62 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝐴) | 
| 95 |  | f1ocnvfv 7299 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥:𝐴–1-1-onto→𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝐴) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))) | 
| 96 | 93, 94, 95 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) = (◡𝑓‘𝑦))) | 
| 97 |  | simplrr 777 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑓‘𝑦) ∈ 𝑡) | 
| 98 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → ((◡𝑥‘𝑦) ∈ 𝑡 ↔ (◡𝑓‘𝑦) ∈ 𝑡)) | 
| 99 | 97, 98 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((◡𝑥‘𝑦) = (◡𝑓‘𝑦) → (◡𝑥‘𝑦) ∈ 𝑡)) | 
| 100 | 96, 99 | syld 47 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) ∧ 𝑥 ∈ (Base‘𝐺)) → ((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) | 
| 101 | 100 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) | 
| 102 |  | fveq1 6904 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑥 → (𝑢‘(◡𝑓‘𝑦)) = (𝑥‘(◡𝑓‘𝑦))) | 
| 103 | 102 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑥 → ((𝑢‘(◡𝑓‘𝑦)) = 𝑦 ↔ (𝑥‘(◡𝑓‘𝑦)) = 𝑦)) | 
| 104 | 103 | ralrab 3698 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
{𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡 ↔ ∀𝑥 ∈ (Base‘𝐺)((𝑥‘(◡𝑓‘𝑦)) = 𝑦 → (◡𝑥‘𝑦) ∈ 𝑡)) | 
| 105 | 101, 104 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡) | 
| 106 |  | ssrab 4072 | . . . . . . . . . . . . . . . . 17
⊢ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} ↔ ({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (Base‘𝐺) ∧ ∀𝑥 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} (◡𝑥‘𝑦) ∈ 𝑡)) | 
| 107 | 91, 105, 106 | sylanbrc 583 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡}) | 
| 108 | 39 | mptpreima 6257 | . . . . . . . . . . . . . . . 16
⊢ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡) = {𝑥 ∈ (Base‘𝐺) ∣ (◡𝑥‘𝑦) ∈ 𝑡} | 
| 109 | 107, 108 | sseqtrrdi 4024 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡)) | 
| 110 |  | funmpt 6603 | . . . . . . . . . . . . . . . 16
⊢ Fun
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) | 
| 111 |  | fvex 6918 | . . . . . . . . . . . . . . . . . 18
⊢ (◡𝑥‘𝑦) ∈ V | 
| 112 | 111, 39 | dmmpti 6711 | . . . . . . . . . . . . . . . . 17
⊢ dom
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) = (Base‘𝐺) | 
| 113 | 91, 112 | sseqtrrdi 4024 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) | 
| 114 |  | funimass3 7073 | . . . . . . . . . . . . . . . 16
⊢ ((Fun
(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∧ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ dom (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))) | 
| 115 | 110, 113,
114 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡 ↔ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ⊆ (◡(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑡))) | 
| 116 | 109, 115 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡) | 
| 117 |  | eleq2 2829 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (𝑓 ∈ 𝑣 ↔ 𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})) | 
| 118 |  | imaeq2 6073 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) = ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦})) | 
| 119 | 118 | sseq1d 4014 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡 ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) | 
| 120 | 117, 119 | anbi12d 632 | . . . . . . . . . . . . . . 15
⊢ (𝑣 = {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} → ((𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡) ↔ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡))) | 
| 121 | 120 | rspcev 3621 | . . . . . . . . . . . . . 14
⊢ (({𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∈ (TopOpen‘𝐺) ∧ (𝑓 ∈ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦} ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ {𝑢 ∈ (Base‘𝐺) ∣ (𝑢‘(◡𝑓‘𝑦)) = 𝑦}) ⊆ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)) | 
| 122 | 81, 89, 116, 121 | syl12anc 836 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ (𝑡 ∈ 𝒫 𝐴 ∧ (◡𝑓‘𝑦) ∈ 𝑡)) → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡)) | 
| 123 | 122 | expr 456 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → ((◡𝑓‘𝑦) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) | 
| 124 | 43, 123 | sylbid 240 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) ∧ 𝑡 ∈ 𝒫 𝐴) → (((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) | 
| 125 | 124 | ralrimiva 3145 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))) | 
| 126 | 24 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (TopOpen‘𝐺) ∈ (TopOn‘(Base‘𝐺))) | 
| 127 | 12 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | 
| 128 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → 𝑓 ∈ (Base‘𝐺)) | 
| 129 |  | iscnp 23246 | . . . . . . . . . . 11
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))))) | 
| 130 | 126, 127,
128, 129 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑡 ∈ 𝒫 𝐴(((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦))‘𝑓) ∈ 𝑡 → ∃𝑣 ∈ (TopOpen‘𝐺)(𝑓 ∈ 𝑣 ∧ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) “ 𝑣) ⊆ 𝑡))))) | 
| 131 | 36, 125, 130 | mpbir2and 713 | . . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑓 ∈ (Base‘𝐺)) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)) | 
| 132 | 131 | ralrimiva 3145 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)) | 
| 133 |  | cncnp 23289 | . . . . . . . . . 10
⊢
(((TopOpen‘𝐺)
∈ (TopOn‘(Base‘𝐺)) ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) | 
| 134 | 24, 12, 133 | syl2anc 584 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) | 
| 135 | 134 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴) ↔ ((𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)):(Base‘𝐺)⟶𝐴 ∧ ∀𝑓 ∈ (Base‘𝐺)(𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ (((TopOpen‘𝐺) CnP 𝒫 𝐴)‘𝑓)))) | 
| 136 | 35, 132, 135 | mpbir2and 713 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn 𝒫 𝐴)) | 
| 137 |  | fvconst2g 7223 | . . . . . . . . 9
⊢
((𝒫 𝐴 ∈
Top ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴) | 
| 138 | 26, 137 | sylan 580 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((𝐴 × {𝒫 𝐴})‘𝑦) = 𝒫 𝐴) | 
| 139 | 138 | oveq2d 7448 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦)) = ((TopOpen‘𝐺) Cn 𝒫 𝐴)) | 
| 140 | 136, 139 | eleqtrrd 2843 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ (Base‘𝐺) ↦ (◡𝑥‘𝑦)) ∈ ((TopOpen‘𝐺) Cn ((𝐴 × {𝒫 𝐴})‘𝑦))) | 
| 141 | 10, 24, 25, 28, 140 | ptcn 23636 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) ∈ ((TopOpen‘𝐺) Cn (∏t‘(𝐴 × {𝒫 𝐴})))) | 
| 142 |  | eqid 2736 | . . . . . . . . 9
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 143 | 5, 142 | grpinvf 19005 | . . . . . . . 8
⊢ (𝐺 ∈ Grp →
(invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) | 
| 144 | 2, 143 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺)) | 
| 145 | 144 | feqmptd 6976 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥))) | 
| 146 | 1, 5, 142 | symginv 19421 | . . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝐺) →
((invg‘𝐺)‘𝑥) = ◡𝑥) | 
| 147 | 146 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = ◡𝑥) | 
| 148 | 32 | feqmptd 6976 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥 = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) | 
| 149 | 147, 148 | eqtrd 2776 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ((invg‘𝐺)‘𝑥) = (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦))) | 
| 150 | 149 | mpteq2dva 5241 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↦ ((invg‘𝐺)‘𝑥)) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))) | 
| 151 | 145, 150 | eqtrd 2776 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) = (𝑥 ∈ (Base‘𝐺) ↦ (𝑦 ∈ 𝐴 ↦ (◡𝑥‘𝑦)))) | 
| 152 |  | xkopt 23664 | . . . . . . 7
⊢
((𝒫 𝐴 ∈
Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 ↑ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) | 
| 153 | 26, 152 | mpancom 688 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑ko 𝒫 𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) | 
| 154 | 153 | oveq2d 7448 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫 𝐴)) = ((TopOpen‘𝐺) Cn
(∏t‘(𝐴 × {𝒫 𝐴})))) | 
| 155 | 141, 151,
154 | 3eltr4d 2855 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴))) | 
| 156 |  | eqid 2736 | . . . . . . 7
⊢
(𝒫 𝐴
↑ko 𝒫 𝐴) = (𝒫 𝐴 ↑ko 𝒫 𝐴) | 
| 157 | 156 | xkotopon 23609 | . . . . . 6
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ Top) → (𝒫 𝐴 ↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) | 
| 158 | 26, 26, 157 | syl2anc 584 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) | 
| 159 |  | frn 6742 | . . . . . 6
⊢
((invg‘𝐺):(Base‘𝐺)⟶(Base‘𝐺) → ran (invg‘𝐺) ⊆ (Base‘𝐺)) | 
| 160 | 2, 143, 159 | 3syl 18 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ran (invg‘𝐺) ⊆ (Base‘𝐺)) | 
| 161 |  | cndis 23300 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑m 𝐴)) | 
| 162 | 12, 161 | mpdan 687 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑m 𝐴)) | 
| 163 | 21, 162 | sseqtrrd 4020 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) | 
| 164 |  | cnrest2 23295 | . . . . 5
⊢
(((𝒫 𝐴
↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (invg‘𝐺) ⊆ (Base‘𝐺) ∧ (Base‘𝐺) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴)) ↔
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn ((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺))))) | 
| 165 | 158, 160,
163, 164 | syl3anc 1372 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴)) ↔
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn ((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝐺))))) | 
| 166 | 155, 165 | mpbid 232 | . . 3
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝐺)))) | 
| 167 | 153 | oveq1d 7447 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝐺))) | 
| 168 | 167, 11 | eqtrd 2776 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺)) =
(TopOpen‘𝐺)) | 
| 169 | 168 | oveq2d 7448 | . . 3
⊢ (𝐴 ∈ 𝑉 → ((TopOpen‘𝐺) Cn ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝐺))) =
((TopOpen‘𝐺) Cn
(TopOpen‘𝐺))) | 
| 170 | 166, 169 | eleqtrd 2842 | . 2
⊢ (𝐴 ∈ 𝑉 → (invg‘𝐺) ∈ ((TopOpen‘𝐺) Cn (TopOpen‘𝐺))) | 
| 171 |  | eqid 2736 | . . 3
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) | 
| 172 | 171, 142 | istgp 24086 | . 2
⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧
(invg‘𝐺)
∈ ((TopOpen‘𝐺)
Cn (TopOpen‘𝐺)))) | 
| 173 | 2, 9, 170, 172 | syl3anbrc 1343 | 1
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp) |