| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | efmndtmd.g | . . 3
⊢ 𝑀 = (EndoFMnd‘𝐴) | 
| 2 | 1 | efmndmnd 18903 | . 2
⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ Mnd) | 
| 3 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) | 
| 4 | 1, 3 | efmndtopn 18897 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝑀)) =
(TopOpen‘𝑀)) | 
| 5 |  | distopon 23005 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | 
| 6 |  | eqid 2736 | . . . . . . 7
⊢
(∏t‘(𝐴 × {𝒫 𝐴})) = (∏t‘(𝐴 × {𝒫 𝐴})) | 
| 7 | 6 | pttoponconst 23606 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) | 
| 8 | 5, 7 | mpdan 687 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴))) | 
| 9 | 1, 3 | efmndbas 18885 | . . . . . . . . 9
⊢
(Base‘𝑀) =
(𝐴 ↑m 𝐴) | 
| 10 | 9 | eleq2i 2832 | . . . . . . . 8
⊢ (𝑥 ∈ (Base‘𝑀) ↔ 𝑥 ∈ (𝐴 ↑m 𝐴)) | 
| 11 | 10 | biimpi 216 | . . . . . . 7
⊢ (𝑥 ∈ (Base‘𝑀) → 𝑥 ∈ (𝐴 ↑m 𝐴)) | 
| 12 | 11 | a1i 11 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝑀) → 𝑥 ∈ (𝐴 ↑m 𝐴))) | 
| 13 | 12 | ssrdv 3988 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (Base‘𝑀) ⊆ (𝐴 ↑m 𝐴)) | 
| 14 |  | resttopon 23170 | . . . . 5
⊢
(((∏t‘(𝐴 × {𝒫 𝐴})) ∈ (TopOn‘(𝐴 ↑m 𝐴)) ∧ (Base‘𝑀) ⊆ (𝐴 ↑m 𝐴)) → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝑀)) ∈
(TopOn‘(Base‘𝑀))) | 
| 15 | 8, 13, 14 | syl2anc 584 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((∏t‘(𝐴 × {𝒫 𝐴})) ↾t
(Base‘𝑀)) ∈
(TopOn‘(Base‘𝑀))) | 
| 16 | 4, 15 | eqeltrrd 2841 | . . 3
⊢ (𝐴 ∈ 𝑉 → (TopOpen‘𝑀) ∈ (TopOn‘(Base‘𝑀))) | 
| 17 |  | eqid 2736 | . . . 4
⊢
(TopOpen‘𝑀) =
(TopOpen‘𝑀) | 
| 18 | 3, 17 | istps 22941 | . . 3
⊢ (𝑀 ∈ TopSp ↔
(TopOpen‘𝑀) ∈
(TopOn‘(Base‘𝑀))) | 
| 19 | 16, 18 | sylibr 234 | . 2
⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ TopSp) | 
| 20 |  | eqid 2736 | . . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) | 
| 21 | 1, 3, 20 | efmndplusg 18894 | . . . . . 6
⊢
(+g‘𝑀) = (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑥 ∘ 𝑦)) | 
| 22 |  | eqid 2736 | . . . . . . 7
⊢
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝑀)) = ((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝑀)) | 
| 23 |  | distop 23003 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) | 
| 24 |  | eqid 2736 | . . . . . . . . 9
⊢
(𝒫 𝐴
↑ko 𝒫 𝐴) = (𝒫 𝐴 ↑ko 𝒫 𝐴) | 
| 25 | 24 | xkotopon 23609 | . . . . . . . 8
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ Top) → (𝒫 𝐴 ↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) | 
| 26 | 23, 23, 25 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫
𝐴 Cn 𝒫 𝐴))) | 
| 27 |  | cndis 23300 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ∈ (TopOn‘𝐴)) → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑m 𝐴)) | 
| 28 | 5, 27 | mpdan 687 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 Cn 𝒫 𝐴) = (𝐴 ↑m 𝐴)) | 
| 29 | 13, 28 | sseqtrrd 4020 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (Base‘𝑀) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) | 
| 30 |  | disllycmp 23507 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Locally Comp) | 
| 31 |  | llynlly 23486 | . . . . . . . . 9
⊢
(𝒫 𝐴 ∈
Locally Comp → 𝒫 𝐴 ∈ 𝑛-Locally
Comp) | 
| 32 | 30, 31 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ 𝑛-Locally
Comp) | 
| 33 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) | 
| 34 | 33 | xkococn 23669 | . . . . . . . 8
⊢
((𝒫 𝐴 ∈
Top ∧ 𝒫 𝐴
∈ 𝑛-Locally Comp ∧ 𝒫 𝐴 ∈ Top) → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ↑ko 𝒫 𝐴) ×t (𝒫
𝐴 ↑ko
𝒫 𝐴)) Cn (𝒫
𝐴 ↑ko
𝒫 𝐴))) | 
| 35 | 23, 32, 23, 34 | syl3anc 1372 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (𝒫 𝐴 Cn 𝒫 𝐴), 𝑦 ∈ (𝒫 𝐴 Cn 𝒫 𝐴) ↦ (𝑥 ∘ 𝑦)) ∈ (((𝒫 𝐴 ↑ko 𝒫 𝐴) ×t (𝒫
𝐴 ↑ko
𝒫 𝐴)) Cn (𝒫
𝐴 ↑ko
𝒫 𝐴))) | 
| 36 | 22, 26, 29, 22, 26, 29, 35 | cnmpt2res 23686 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝑀), 𝑦 ∈ (Base‘𝑀) ↦ (𝑥 ∘ 𝑦)) ∈ ((((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴))) | 
| 37 | 21, 36 | eqeltrid 2844 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (+g‘𝑀) ∈ ((((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝑀))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴))) | 
| 38 |  | xkopt 23664 | . . . . . . . . . 10
⊢
((𝒫 𝐴 ∈
Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 ↑ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) | 
| 39 | 23, 38 | mpancom 688 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ↑ko 𝒫 𝐴) =
(∏t‘(𝐴 × {𝒫 𝐴}))) | 
| 40 | 39 | oveq1d 7447 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀)) =
((∏t‘(𝐴 × {𝒫 𝐴})) ↾t (Base‘𝑀))) | 
| 41 | 40, 4 | eqtrd 2776 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀)) =
(TopOpen‘𝑀)) | 
| 42 | 41, 41 | oveq12d 7450 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))) =
((TopOpen‘𝑀)
×t (TopOpen‘𝑀))) | 
| 43 | 42 | oveq1d 7447 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ((((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))
×t ((𝒫 𝐴 ↑ko 𝒫 𝐴) ↾t
(Base‘𝑀))) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴)) = (((TopOpen‘𝑀) ×t (TopOpen‘𝑀)) Cn (𝒫 𝐴 ↑ko 𝒫
𝐴))) | 
| 44 | 37, 43 | eleqtrd 2842 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴))) | 
| 45 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 46 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑦 ∈ V | 
| 47 | 45, 46 | coex 7953 | . . . . . . . . . 10
⊢ (𝑥 ∘ 𝑦) ∈ V | 
| 48 | 21, 47 | fnmpoi 8096 | . . . . . . . . 9
⊢
(+g‘𝑀) Fn ((Base‘𝑀) × (Base‘𝑀)) | 
| 49 |  | eqid 2736 | . . . . . . . . . 10
⊢
(+𝑓‘𝑀) = (+𝑓‘𝑀) | 
| 50 | 3, 20, 49 | plusfeq 18662 | . . . . . . . . 9
⊢
((+g‘𝑀) Fn ((Base‘𝑀) × (Base‘𝑀)) → (+𝑓‘𝑀) = (+g‘𝑀)) | 
| 51 | 48, 50 | ax-mp 5 | . . . . . . . 8
⊢
(+𝑓‘𝑀) = (+g‘𝑀) | 
| 52 | 51 | eqcomi 2745 | . . . . . . 7
⊢
(+g‘𝑀) = (+𝑓‘𝑀) | 
| 53 | 3, 52 | mndplusf 18766 | . . . . . 6
⊢ (𝑀 ∈ Mnd →
(+g‘𝑀):((Base‘𝑀) × (Base‘𝑀))⟶(Base‘𝑀)) | 
| 54 |  | frn 6742 | . . . . . 6
⊢
((+g‘𝑀):((Base‘𝑀) × (Base‘𝑀))⟶(Base‘𝑀) → ran (+g‘𝑀) ⊆ (Base‘𝑀)) | 
| 55 | 2, 53, 54 | 3syl 18 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ran (+g‘𝑀) ⊆ (Base‘𝑀)) | 
| 56 |  | cnrest2 23295 | . . . . 5
⊢
(((𝒫 𝐴
↑ko 𝒫 𝐴) ∈ (TopOn‘(𝒫 𝐴 Cn 𝒫 𝐴)) ∧ ran (+g‘𝑀) ⊆ (Base‘𝑀) ∧ (Base‘𝑀) ⊆ (𝒫 𝐴 Cn 𝒫 𝐴)) → ((+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴)) ↔ (+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝑀))))) | 
| 57 | 26, 55, 29, 56 | syl3anc 1372 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
(𝒫 𝐴
↑ko 𝒫 𝐴)) ↔ (+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝑀))))) | 
| 58 | 44, 57 | mpbid 232 | . . 3
⊢ (𝐴 ∈ 𝑉 → (+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
((𝒫 𝐴
↑ko 𝒫 𝐴) ↾t (Base‘𝑀)))) | 
| 59 | 41 | oveq2d 7448 | . . 3
⊢ (𝐴 ∈ 𝑉 → (((TopOpen‘𝑀) ×t (TopOpen‘𝑀)) Cn ((𝒫 𝐴 ↑ko 𝒫
𝐴) ↾t
(Base‘𝑀))) =
(((TopOpen‘𝑀)
×t (TopOpen‘𝑀)) Cn (TopOpen‘𝑀))) | 
| 60 | 58, 59 | eleqtrd 2842 | . 2
⊢ (𝐴 ∈ 𝑉 → (+g‘𝑀) ∈ (((TopOpen‘𝑀) ×t
(TopOpen‘𝑀)) Cn
(TopOpen‘𝑀))) | 
| 61 | 52, 17 | istmd 24083 | . 2
⊢ (𝑀 ∈ TopMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ TopSp ∧
(+g‘𝑀)
∈ (((TopOpen‘𝑀)
×t (TopOpen‘𝑀)) Cn (TopOpen‘𝑀)))) | 
| 62 | 2, 19, 60, 61 | syl3anbrc 1343 | 1
⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd) |