| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prdstgpd.y | . . 3
⊢ 𝑌 = (𝑆Xs𝑅) | 
| 2 |  | prdstgpd.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 3 |  | prdstgpd.s | . . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) | 
| 4 |  | prdstgpd.r | . . . 4
⊢ (𝜑 → 𝑅:𝐼⟶TopGrp) | 
| 5 |  | tgpgrp 24087 | . . . . 5
⊢ (𝑥 ∈ TopGrp → 𝑥 ∈ Grp) | 
| 6 | 5 | ssriv 3986 | . . . 4
⊢ TopGrp
⊆ Grp | 
| 7 |  | fss 6751 | . . . 4
⊢ ((𝑅:𝐼⟶TopGrp ∧ TopGrp ⊆ Grp)
→ 𝑅:𝐼⟶Grp) | 
| 8 | 4, 6, 7 | sylancl 586 | . . 3
⊢ (𝜑 → 𝑅:𝐼⟶Grp) | 
| 9 | 1, 2, 3, 8 | prdsgrpd 19069 | . 2
⊢ (𝜑 → 𝑌 ∈ Grp) | 
| 10 |  | tgptmd 24088 | . . . . 5
⊢ (𝑥 ∈ TopGrp → 𝑥 ∈ TopMnd) | 
| 11 | 10 | ssriv 3986 | . . . 4
⊢ TopGrp
⊆ TopMnd | 
| 12 |  | fss 6751 | . . . 4
⊢ ((𝑅:𝐼⟶TopGrp ∧ TopGrp ⊆ TopMnd)
→ 𝑅:𝐼⟶TopMnd) | 
| 13 | 4, 11, 12 | sylancl 586 | . . 3
⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) | 
| 14 | 1, 2, 3, 13 | prdstmdd 24133 | . 2
⊢ (𝜑 → 𝑌 ∈ TopMnd) | 
| 15 |  | eqid 2736 | . . . 4
⊢
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅)) | 
| 16 |  | eqid 2736 | . . . . . 6
⊢
(TopOpen‘𝑌) =
(TopOpen‘𝑌) | 
| 17 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 18 | 16, 17 | tmdtopon 24090 | . . . . 5
⊢ (𝑌 ∈ TopMnd →
(TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) | 
| 19 | 14, 18 | syl 17 | . . . 4
⊢ (𝜑 → (TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) | 
| 20 |  | topnfn 17471 | . . . . . 6
⊢ TopOpen
Fn V | 
| 21 | 4 | ffnd 6736 | . . . . . . 7
⊢ (𝜑 → 𝑅 Fn 𝐼) | 
| 22 |  | dffn2 6737 | . . . . . . 7
⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V) | 
| 23 | 21, 22 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝑅:𝐼⟶V) | 
| 24 |  | fnfco 6772 | . . . . . 6
⊢ ((TopOpen
Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen
∘ 𝑅) Fn 𝐼) | 
| 25 | 20, 23, 24 | sylancr 587 | . . . . 5
⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼) | 
| 26 |  | fvco3 7007 | . . . . . . . 8
⊢ ((𝑅:𝐼⟶TopGrp ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) | 
| 27 | 4, 26 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) | 
| 28 | 4 | ffvelcdmda 7103 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑅‘𝑦) ∈ TopGrp) | 
| 29 |  | eqid 2736 | . . . . . . . . 9
⊢
(TopOpen‘(𝑅‘𝑦)) = (TopOpen‘(𝑅‘𝑦)) | 
| 30 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) | 
| 31 | 29, 30 | tgptopon 24091 | . . . . . . . 8
⊢ ((𝑅‘𝑦) ∈ TopGrp → (TopOpen‘(𝑅‘𝑦)) ∈ (TopOn‘(Base‘(𝑅‘𝑦)))) | 
| 32 |  | topontop 22920 | . . . . . . . 8
⊢
((TopOpen‘(𝑅‘𝑦)) ∈ (TopOn‘(Base‘(𝑅‘𝑦))) → (TopOpen‘(𝑅‘𝑦)) ∈ Top) | 
| 33 | 28, 31, 32 | 3syl 18 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘(𝑅‘𝑦)) ∈ Top) | 
| 34 | 27, 33 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top) | 
| 35 | 34 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top) | 
| 36 |  | ffnfv 7138 | . . . . 5
⊢ ((TopOpen
∘ 𝑅):𝐼⟶Top ↔ ((TopOpen
∘ 𝑅) Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 ((TopOpen ∘ 𝑅)‘𝑦) ∈ Top)) | 
| 37 | 25, 35, 36 | sylanbrc 583 | . . . 4
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) | 
| 38 | 19 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) | 
| 39 | 1, 3, 2, 21, 16 | prdstopn 23637 | . . . . . . . . . . . 12
⊢ (𝜑 → (TopOpen‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen‘𝑌) = (∏t‘(TopOpen
∘ 𝑅))) | 
| 41 | 40 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(TopOpen‘𝑌)) | 
| 42 | 41, 38 | eqeltrd 2840 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) ∈
(TopOn‘(Base‘𝑌))) | 
| 43 |  | toponuni 22921 | . . . . . . . . 9
⊢
((∏t‘(TopOpen ∘ 𝑅)) ∈ (TopOn‘(Base‘𝑌)) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) | 
| 44 |  | mpteq1 5234 | . . . . . . . . 9
⊢
((Base‘𝑌) =
∪ (∏t‘(TopOpen ∘ 𝑅)) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦))) | 
| 45 | 42, 43, 44 | 3syl 18 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦))) | 
| 46 | 2 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ 𝑊) | 
| 47 | 37 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (TopOpen ∘ 𝑅):𝐼⟶Top) | 
| 48 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ 𝐼) | 
| 49 |  | eqid 2736 | . . . . . . . . . 10
⊢ ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (∏t‘(TopOpen ∘ 𝑅)) | 
| 50 | 49, 15 | ptpjcn 23620 | . . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅):𝐼⟶Top ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) | 
| 51 | 46, 47, 48, 50 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) | 
| 52 | 45, 51 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦))) | 
| 53 | 41, 27 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑦)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) | 
| 54 | 52, 53 | eleqtrd 2842 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑦)) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) | 
| 55 |  | eqid 2736 | . . . . . . . 8
⊢
(invg‘(𝑅‘𝑦)) = (invg‘(𝑅‘𝑦)) | 
| 56 | 29, 55 | tgpinv 24094 | . . . . . . 7
⊢ ((𝑅‘𝑦) ∈ TopGrp →
(invg‘(𝑅‘𝑦)) ∈ ((TopOpen‘(𝑅‘𝑦)) Cn (TopOpen‘(𝑅‘𝑦)))) | 
| 57 | 28, 56 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (invg‘(𝑅‘𝑦)) ∈ ((TopOpen‘(𝑅‘𝑦)) Cn (TopOpen‘(𝑅‘𝑦)))) | 
| 58 | 38, 54, 57 | cnmpt11f 23673 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) | 
| 59 | 27 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen‘𝑌) Cn ((TopOpen ∘ 𝑅)‘𝑦)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑦)))) | 
| 60 | 58, 59 | eleqtrrd 2843 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))) ∈ ((TopOpen‘𝑌) Cn ((TopOpen ∘ 𝑅)‘𝑦))) | 
| 61 | 15, 19, 2, 37, 60 | ptcn 23636 | . . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦)))) ∈ ((TopOpen‘𝑌) Cn (∏t‘(TopOpen
∘ 𝑅)))) | 
| 62 |  | eqid 2736 | . . . . . . 7
⊢
(invg‘𝑌) = (invg‘𝑌) | 
| 63 | 17, 62 | grpinvf 19005 | . . . . . 6
⊢ (𝑌 ∈ Grp →
(invg‘𝑌):(Base‘𝑌)⟶(Base‘𝑌)) | 
| 64 | 9, 63 | syl 17 | . . . . 5
⊢ (𝜑 →
(invg‘𝑌):(Base‘𝑌)⟶(Base‘𝑌)) | 
| 65 | 64 | feqmptd 6976 | . . . 4
⊢ (𝜑 →
(invg‘𝑌) =
(𝑥 ∈ (Base‘𝑌) ↦
((invg‘𝑌)‘𝑥))) | 
| 66 | 2 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝐼 ∈ 𝑊) | 
| 67 | 3 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑆 ∈ 𝑉) | 
| 68 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑅:𝐼⟶Grp) | 
| 69 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → 𝑥 ∈ (Base‘𝑌)) | 
| 70 | 1, 66, 67, 68, 17, 62, 69 | prdsinvgd 19070 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑌)) → ((invg‘𝑌)‘𝑥) = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦)))) | 
| 71 | 70 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑌) ↦ ((invg‘𝑌)‘𝑥)) = (𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))))) | 
| 72 | 65, 71 | eqtrd 2776 | . . 3
⊢ (𝜑 →
(invg‘𝑌) =
(𝑥 ∈ (Base‘𝑌) ↦ (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝑥‘𝑦))))) | 
| 73 | 39 | oveq2d 7448 | . . 3
⊢ (𝜑 → ((TopOpen‘𝑌) Cn (TopOpen‘𝑌)) = ((TopOpen‘𝑌) Cn
(∏t‘(TopOpen ∘ 𝑅)))) | 
| 74 | 61, 72, 73 | 3eltr4d 2855 | . 2
⊢ (𝜑 →
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (TopOpen‘𝑌))) | 
| 75 | 16, 62 | istgp 24086 | . 2
⊢ (𝑌 ∈ TopGrp ↔ (𝑌 ∈ Grp ∧ 𝑌 ∈ TopMnd ∧
(invg‘𝑌)
∈ ((TopOpen‘𝑌)
Cn (TopOpen‘𝑌)))) | 
| 76 | 9, 14, 74, 75 | syl3anbrc 1343 | 1
⊢ (𝜑 → 𝑌 ∈ TopGrp) |