| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑤 = ∅ → (𝐵 ↑m 𝑤) = (𝐵 ↑m
∅)) | 
| 2 | 1 | mpteq1d 5236 | . . . . . . 7
⊢ (𝑤 = ∅ → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg
𝑥))) | 
| 3 |  | xpeq1 5698 | . . . . . . . . . 10
⊢ (𝑤 = ∅ → (𝑤 × {𝐽}) = (∅ × {𝐽})) | 
| 4 |  | 0xp 5783 | . . . . . . . . . 10
⊢ (∅
× {𝐽}) =
∅ | 
| 5 | 3, 4 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤 × {𝐽}) = ∅) | 
| 6 | 5 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = ∅ →
(∏t‘(𝑤 × {𝐽})) =
(∏t‘∅)) | 
| 7 | 6 | oveq1d 7447 | . . . . . . 7
⊢ (𝑤 = ∅ →
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘∅) Cn
𝐽)) | 
| 8 | 2, 7 | eleq12d 2834 | . . . . . 6
⊢ (𝑤 = ∅ → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg
𝑥)) ∈
((∏t‘∅) Cn 𝐽))) | 
| 9 | 8 | imbi2d 340 | . . . . 5
⊢ (𝑤 = ∅ → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg
𝑥)) ∈
((∏t‘∅) Cn 𝐽)))) | 
| 10 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝐵 ↑m 𝑤) = (𝐵 ↑m 𝑦)) | 
| 11 | 10 | mpteq1d 5236 | . . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥))) | 
| 12 |  | xpeq1 5698 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 × {𝐽}) = (𝑦 × {𝐽})) | 
| 13 | 12 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → (∏t‘(𝑤 × {𝐽})) = (∏t‘(𝑦 × {𝐽}))) | 
| 14 | 13 | oveq1d 7447 | . . . . . . 7
⊢ (𝑤 = 𝑦 → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) | 
| 15 | 11, 14 | eleq12d 2834 | . . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽))) | 
| 16 | 15 | imbi2d 340 | . . . . 5
⊢ (𝑤 = 𝑦 → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)))) | 
| 17 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐵 ↑m 𝑤) = (𝐵 ↑m (𝑦 ∪ {𝑧}))) | 
| 18 | 17 | mpteq1d 5236 | . . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥))) | 
| 19 |  | xpeq1 5698 | . . . . . . . . 9
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 × {𝐽}) = ((𝑦 ∪ {𝑧}) × {𝐽})) | 
| 20 | 19 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∏t‘(𝑤 × {𝐽})) = (∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))) | 
| 21 | 20 | oveq1d 7447 | . . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 22 | 18, 21 | eleq12d 2834 | . . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))) | 
| 23 | 22 | imbi2d 340 | . . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))) | 
| 24 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑤 = 𝐴 → (𝐵 ↑m 𝑤) = (𝐵 ↑m 𝐴)) | 
| 25 | 24 | mpteq1d 5236 | . . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥))) | 
| 26 |  | xpeq1 5698 | . . . . . . . . 9
⊢ (𝑤 = 𝐴 → (𝑤 × {𝐽}) = (𝐴 × {𝐽})) | 
| 27 | 26 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑤 = 𝐴 → (∏t‘(𝑤 × {𝐽})) = (∏t‘(𝐴 × {𝐽}))) | 
| 28 | 27 | oveq1d 7447 | . . . . . . 7
⊢ (𝑤 = 𝐴 → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)) | 
| 29 | 25, 28 | eleq12d 2834 | . . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽))) | 
| 30 | 29 | imbi2d 340 | . . . . 5
⊢ (𝑤 = 𝐴 → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽)))) | 
| 31 |  | elmapfn 8906 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑m ∅) → 𝑥 Fn ∅) | 
| 32 |  | fn0 6698 | . . . . . . . . . 10
⊢ (𝑥 Fn ∅ ↔ 𝑥 = ∅) | 
| 33 | 31, 32 | sylib 218 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ↑m ∅) → 𝑥 = ∅) | 
| 34 | 33 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ↑m ∅) → (𝐺 Σg
𝑥) = (𝐺 Σg
∅)) | 
| 35 |  | eqid 2736 | . . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 36 | 35 | gsum0 18698 | . . . . . . . 8
⊢ (𝐺 Σg
∅) = (0g‘𝐺) | 
| 37 | 34, 36 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑥 ∈ (𝐵 ↑m ∅) → (𝐺 Σg
𝑥) =
(0g‘𝐺)) | 
| 38 | 37 | mpteq2ia 5244 | . . . . . 6
⊢ (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg
𝑥)) = (𝑥 ∈ (𝐵 ↑m ∅) ↦
(0g‘𝐺)) | 
| 39 |  | 0ex 5306 | . . . . . . . 8
⊢ ∅
∈ V | 
| 40 |  | tmdgsum.j | . . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) | 
| 41 |  | tmdgsum.b | . . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) | 
| 42 | 40, 41 | tmdtopon 24090 | . . . . . . . . 9
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) | 
| 43 | 42 | adantl 481 | . . . . . . . 8
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → 𝐽 ∈ (TopOn‘𝐵)) | 
| 44 | 4 | fveq2i 6908 | . . . . . . . . . 10
⊢
(∏t‘(∅ × {𝐽})) =
(∏t‘∅) | 
| 45 | 44 | eqcomi 2745 | . . . . . . . . 9
⊢
(∏t‘∅) = (∏t‘(∅
× {𝐽})) | 
| 46 | 45 | pttoponconst 23606 | . . . . . . . 8
⊢ ((∅
∈ V ∧ 𝐽 ∈
(TopOn‘𝐵)) →
(∏t‘∅) ∈ (TopOn‘(𝐵 ↑m
∅))) | 
| 47 | 39, 43, 46 | sylancr 587 | . . . . . . 7
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) →
(∏t‘∅) ∈ (TopOn‘(𝐵 ↑m
∅))) | 
| 48 |  | tmdmnd 24084 | . . . . . . . . 9
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) | 
| 49 | 48 | adantl 481 | . . . . . . . 8
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → 𝐺 ∈ Mnd) | 
| 50 | 41, 35 | mndidcl 18763 | . . . . . . . 8
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) | 
| 51 | 49, 50 | syl 17 | . . . . . . 7
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) →
(0g‘𝐺)
∈ 𝐵) | 
| 52 | 47, 43, 51 | cnmptc 23671 | . . . . . 6
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m ∅) ↦
(0g‘𝐺))
∈ ((∏t‘∅) Cn 𝐽)) | 
| 53 | 38, 52 | eqeltrid 2844 | . . . . 5
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg
𝑥)) ∈
((∏t‘∅) Cn 𝐽)) | 
| 54 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑤)) | 
| 55 | 54 | cbvmptv 5254 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑤)) | 
| 56 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 57 |  | simpl1l 1224 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝐺 ∈ CMnd) | 
| 58 |  | simp2l 1199 | . . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑦 ∈ Fin) | 
| 59 |  | snfi 9084 | . . . . . . . . . . . . . 14
⊢ {𝑧} ∈ Fin | 
| 60 |  | unfi 9212 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 61 | 58, 59, 60 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 62 | 61 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑦 ∪ {𝑧}) ∈ Fin) | 
| 63 |  | elmapi 8890 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) → 𝑤:(𝑦 ∪ {𝑧})⟶𝐵) | 
| 64 | 63 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑤:(𝑦 ∪ {𝑧})⟶𝐵) | 
| 65 |  | fvexd 6920 | . . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (0g‘𝐺) ∈ V) | 
| 66 | 64, 62, 65 | fdmfifsupp 9416 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑤 finSupp (0g‘𝐺)) | 
| 67 |  | simpl2r 1227 | . . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → ¬ 𝑧 ∈ 𝑦) | 
| 68 |  | disjsn 4710 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) | 
| 69 | 67, 68 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑦 ∩ {𝑧}) = ∅) | 
| 70 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧})) | 
| 71 | 41, 35, 56, 57, 62, 64, 66, 69, 70 | gsumsplit 19947 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg 𝑤) = ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))) | 
| 72 | 71 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑤)) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧}))))) | 
| 73 | 55, 72 | eqtrid 2788 | . . . . . . . . 9
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧}))))) | 
| 74 |  | simp1r 1198 | . . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐺 ∈ TopMnd) | 
| 75 | 74, 42 | syl 17 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐵)) | 
| 76 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) = (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) | 
| 77 | 76 | pttoponconst 23606 | . . . . . . . . . . 11
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐽 ∈ (TopOn‘𝐵)) → (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑m (𝑦 ∪ {𝑧})))) | 
| 78 | 61, 75, 77 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑m (𝑦 ∪ {𝑧})))) | 
| 79 |  | toponuni 22921 | . . . . . . . . . . . . . 14
⊢
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐵 ↑m (𝑦 ∪ {𝑧})) = ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))) | 
| 80 | 78, 79 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝐵 ↑m (𝑦 ∪ {𝑧})) = ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))) | 
| 81 | 80 | mpteq1d 5236 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤 ↾ 𝑦)) = (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦))) | 
| 82 |  | topontop 22920 | . . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | 
| 83 | 74, 42, 82 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐽 ∈ Top) | 
| 84 |  | fconst6g 6796 | . . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Top → ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top) | 
| 86 |  | ssun1 4177 | . . . . . . . . . . . . . 14
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) | 
| 87 | 86 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑦 ⊆ (𝑦 ∪ {𝑧})) | 
| 88 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) = ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) | 
| 89 |  | xpssres 6035 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) = (𝑦 × {𝐽})) | 
| 90 | 86, 89 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) = (𝑦 × {𝐽}) | 
| 91 | 90 | eqcomi 2745 | . . . . . . . . . . . . . . 15
⊢ (𝑦 × {𝐽}) = (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) | 
| 92 | 91 | fveq2i 6908 | . . . . . . . . . . . . . 14
⊢
(∏t‘(𝑦 × {𝐽})) = (∏t‘(((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦)) | 
| 93 | 88, 76, 92 | ptrescn 23648 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽})))) | 
| 94 | 61, 85, 87, 93 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽})))) | 
| 95 | 81, 94 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽})))) | 
| 96 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(∏t‘(𝑦 × {𝐽})) = (∏t‘(𝑦 × {𝐽})) | 
| 97 | 96 | pttoponconst 23606 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ 𝐽 ∈ (TopOn‘𝐵)) →
(∏t‘(𝑦 × {𝐽})) ∈ (TopOn‘(𝐵 ↑m 𝑦))) | 
| 98 | 58, 75, 97 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (∏t‘(𝑦 × {𝐽})) ∈ (TopOn‘(𝐵 ↑m 𝑦))) | 
| 99 |  | simp3 1138 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) | 
| 100 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑤 ↾ 𝑦) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑤 ↾ 𝑦))) | 
| 101 | 78, 95, 98, 99, 100 | cnmpt11 23672 | . . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ 𝑦))) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 102 | 64 | feqmptd 6976 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑤 = (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘))) | 
| 103 | 102 | reseq1d 5995 | . . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑤 ↾ {𝑧}) = ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧})) | 
| 104 |  | ssun2 4178 | . . . . . . . . . . . . . . . 16
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) | 
| 105 |  | resmpt 6054 | . . . . . . . . . . . . . . . 16
⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) | 
| 106 | 104, 105 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘)) | 
| 107 | 103, 106 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑤 ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) | 
| 108 | 107 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑤 ↾ {𝑧})) = (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘)))) | 
| 109 |  | cmnmnd 19816 | . . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | 
| 110 | 57, 109 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝐺 ∈ Mnd) | 
| 111 |  | vex 3483 | . . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V | 
| 112 | 111 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑧 ∈ V) | 
| 113 |  | vsnid 4662 | . . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ {𝑧} | 
| 114 |  | elun2 4182 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧})) | 
| 115 | 113, 114 | mp1i 13 | . . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑧 ∈ (𝑦 ∪ {𝑧})) | 
| 116 | 64, 115 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑤‘𝑧) ∈ 𝐵) | 
| 117 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑤‘𝑘) = (𝑤‘𝑧)) | 
| 118 | 41, 117 | gsumsn 19973 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ V ∧ (𝑤‘𝑧) ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) = (𝑤‘𝑧)) | 
| 119 | 110, 112,
116, 118 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) = (𝑤‘𝑧)) | 
| 120 | 108, 119 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑤 ↾ {𝑧})) = (𝑤‘𝑧)) | 
| 121 | 120 | mpteq2dva 5241 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ {𝑧}))) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧))) | 
| 122 | 80 | mpteq1d 5236 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) = (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧))) | 
| 123 | 113, 114 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑧 ∈ (𝑦 ∪ {𝑧})) | 
| 124 | 88, 76 | ptpjcn 23620 | . . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧))) | 
| 125 | 61, 85, 123, 124 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧))) | 
| 126 | 122, 125 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧))) | 
| 127 |  | fvconst2g 7223 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧) = 𝐽) | 
| 128 | 83, 123, 127 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧) = 𝐽) | 
| 129 | 128 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧)) = ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 130 | 126, 129 | eleqtrd 2842 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 131 | 121, 130 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ {𝑧}))) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 132 | 40, 56, 74, 78, 101, 131 | cnmpt1plusg 24096 | . . . . . . . . 9
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 133 | 73, 132 | eqeltrd 2840 | . . . . . . . 8
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) | 
| 134 | 133 | 3expia 1121 | . . . . . . 7
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))) | 
| 135 | 134 | expcom 413 | . . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → ((𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))) | 
| 136 | 135 | a2d 29 | . . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))) | 
| 137 | 9, 16, 23, 30, 53, 136 | findcard2s 9206 | . . . 4
⊢ (𝐴 ∈ Fin → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽))) | 
| 138 | 137 | com12 32 | . . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝐴 ∈ Fin → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽))) | 
| 139 | 138 | 3impia 1117 | . 2
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽)) | 
| 140 | 42, 82 | syl 17 | . . . . 5
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ Top) | 
| 141 |  | xkopt 23664 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) | 
| 142 | 140, 141 | sylan 580 | . . . 4
⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) | 
| 143 | 142 | 3adant1 1130 | . . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) | 
| 144 | 143 | oveq1d 7447 | . 2
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → ((𝐽 ↑ko 𝒫
𝐴) Cn 𝐽) = ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)) | 
| 145 | 139, 144 | eleqtrrd 2843 | 1
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽)) |