| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prdstopn.y | . . . . . 6
⊢ 𝑌 = (𝑆Xs𝑅) | 
| 2 |  | prdstopn.s | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ 𝑉) | 
| 3 |  | prdstopn.r | . . . . . . 7
⊢ (𝜑 → 𝑅 Fn 𝐼) | 
| 4 |  | prdstopn.i | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 5 |  | fnex 7238 | . . . . . . 7
⊢ ((𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊) → 𝑅 ∈ V) | 
| 6 | 3, 4, 5 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ V) | 
| 7 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 8 |  | eqidd 2737 | . . . . . 6
⊢ (𝜑 → dom 𝑅 = dom 𝑅) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢
(TopSet‘𝑌) =
(TopSet‘𝑌) | 
| 10 | 1, 2, 6, 7, 8, 9 | prdstset 17512 | . . . . 5
⊢ (𝜑 → (TopSet‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) | 
| 11 |  | topnfn 17471 | . . . . . . . . . . 11
⊢ TopOpen
Fn V | 
| 12 |  | dffn2 6737 | . . . . . . . . . . . 12
⊢ (𝑅 Fn 𝐼 ↔ 𝑅:𝐼⟶V) | 
| 13 | 3, 12 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅:𝐼⟶V) | 
| 14 |  | fnfco 6772 | . . . . . . . . . . 11
⊢ ((TopOpen
Fn V ∧ 𝑅:𝐼⟶V) → (TopOpen
∘ 𝑅) Fn 𝐼) | 
| 15 | 11, 13, 14 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (TopOpen ∘ 𝑅) Fn 𝐼) | 
| 16 |  | eqid 2736 | . . . . . . . . . . 11
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} | 
| 17 | 16 | ptval 23579 | . . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅) Fn 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(topGen‘{𝑥 ∣
∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))})) | 
| 18 | 4, 15, 17 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 →
(∏t‘(TopOpen ∘ 𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))})) | 
| 19 | 18 | unieqd 4919 | . . . . . . . 8
⊢ (𝜑 → ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))})) | 
| 20 |  | fvco2 7005 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 Fn 𝐼 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) | 
| 21 | 3, 20 | sylan 580 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) = (TopOpen‘(𝑅‘𝑦))) | 
| 22 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘(𝑅‘𝑦)) = (Base‘(𝑅‘𝑦)) | 
| 23 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(TopSet‘(𝑅‘𝑦)) = (TopSet‘(𝑅‘𝑦)) | 
| 24 | 22, 23 | topnval 17480 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((TopSet‘(𝑅‘𝑦)) ↾t (Base‘(𝑅‘𝑦))) = (TopOpen‘(𝑅‘𝑦)) | 
| 25 |  | restsspw 17477 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((TopSet‘(𝑅‘𝑦)) ↾t (Base‘(𝑅‘𝑦))) ⊆ 𝒫 (Base‘(𝑅‘𝑦)) | 
| 26 | 24, 25 | eqsstrri 4030 | . . . . . . . . . . . . . . . . . . . 20
⊢
(TopOpen‘(𝑅‘𝑦)) ⊆ 𝒫 (Base‘(𝑅‘𝑦)) | 
| 27 | 21, 26 | eqsstrdi 4027 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑦) ⊆ 𝒫 (Base‘(𝑅‘𝑦))) | 
| 28 | 27 | sseld 3981 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) → (𝑔‘𝑦) ∈ 𝒫 (Base‘(𝑅‘𝑦)))) | 
| 29 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑔‘𝑦) ∈ V | 
| 30 | 29 | elpw 4603 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔‘𝑦) ∈ 𝒫 (Base‘(𝑅‘𝑦)) ↔ (𝑔‘𝑦) ⊆ (Base‘(𝑅‘𝑦))) | 
| 31 | 28, 30 | imbitrdi 251 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) → (𝑔‘𝑦) ⊆ (Base‘(𝑅‘𝑦)))) | 
| 32 | 31 | ralimdva 3166 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) → ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ⊆ (Base‘(𝑅‘𝑦)))) | 
| 33 |  | simpl2 1192 | . . . . . . . . . . . . . . . 16
⊢ (((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦)) → ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦)) | 
| 34 | 32, 33 | impel 505 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))) → ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ⊆ (Base‘(𝑅‘𝑦))) | 
| 35 |  | ss2ixp 8951 | . . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝐼 (𝑔‘𝑦) ⊆ (Base‘(𝑅‘𝑦)) → X𝑦 ∈ 𝐼 (𝑔‘𝑦) ⊆ X𝑦 ∈ 𝐼 (Base‘(𝑅‘𝑦))) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))) → X𝑦 ∈ 𝐼 (𝑔‘𝑦) ⊆ X𝑦 ∈ 𝐼 (Base‘(𝑅‘𝑦))) | 
| 37 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))) → 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦)) | 
| 38 | 1, 7, 2, 4, 3 | prdsbas2 17515 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝑌) = X𝑦 ∈
𝐼 (Base‘(𝑅‘𝑦))) | 
| 39 | 38 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))) → (Base‘𝑌) = X𝑦 ∈ 𝐼 (Base‘(𝑅‘𝑦))) | 
| 40 | 36, 37, 39 | 3sstr4d 4038 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))) → 𝑥 ⊆ (Base‘𝑌)) | 
| 41 | 40 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦)) → 𝑥 ⊆ (Base‘𝑌))) | 
| 42 | 41 | exlimdv 1932 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦)) → 𝑥 ⊆ (Base‘𝑌))) | 
| 43 |  | velpw 4604 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫
(Base‘𝑌) ↔ 𝑥 ⊆ (Base‘𝑌)) | 
| 44 | 42, 43 | imbitrrdi 252 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦)) → 𝑥 ∈ 𝒫 (Base‘𝑌))) | 
| 45 | 44 | abssdv 4067 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ⊆ 𝒫 (Base‘𝑌)) | 
| 46 |  | fvex 6918 | . . . . . . . . . . 11
⊢
(Base‘𝑌)
∈ V | 
| 47 | 46 | pwex 5379 | . . . . . . . . . 10
⊢ 𝒫
(Base‘𝑌) ∈
V | 
| 48 | 47 | ssex 5320 | . . . . . . . . 9
⊢ ({𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ⊆ 𝒫 (Base‘𝑌) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ∈ V) | 
| 49 |  | unitg 22975 | . . . . . . . . 9
⊢ ({𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ∈ V → ∪ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))}) = ∪ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))}) | 
| 50 | 45, 48, 49 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → ∪ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))}) = ∪ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))}) | 
| 51 | 19, 50 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ {𝑥
∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))}) | 
| 52 |  | sspwuni 5099 | . . . . . . . 8
⊢ ({𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ⊆ 𝒫 (Base‘𝑌) ↔ ∪ {𝑥
∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ⊆ (Base‘𝑌)) | 
| 53 | 45, 52 | sylib 218 | . . . . . . 7
⊢ (𝜑 → ∪ {𝑥
∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝑔‘𝑦) ∈ ((TopOpen ∘ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((TopOpen
∘ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐼 (𝑔‘𝑦))} ⊆ (Base‘𝑌)) | 
| 54 | 51, 53 | eqsstrd 4017 | . . . . . 6
⊢ (𝜑 → ∪ (∏t‘(TopOpen ∘ 𝑅)) ⊆ (Base‘𝑌)) | 
| 55 |  | sspwuni 5099 | . . . . . 6
⊢
((∏t‘(TopOpen ∘ 𝑅)) ⊆ 𝒫 (Base‘𝑌) ↔ ∪ (∏t‘(TopOpen ∘ 𝑅)) ⊆ (Base‘𝑌)) | 
| 56 | 54, 55 | sylibr 234 | . . . . 5
⊢ (𝜑 →
(∏t‘(TopOpen ∘ 𝑅)) ⊆ 𝒫 (Base‘𝑌)) | 
| 57 | 10, 56 | eqsstrd 4017 | . . . 4
⊢ (𝜑 → (TopSet‘𝑌) ⊆ 𝒫
(Base‘𝑌)) | 
| 58 | 7, 9 | topnid 17481 | . . . 4
⊢
((TopSet‘𝑌)
⊆ 𝒫 (Base‘𝑌) → (TopSet‘𝑌) = (TopOpen‘𝑌)) | 
| 59 | 57, 58 | syl 17 | . . 3
⊢ (𝜑 → (TopSet‘𝑌) = (TopOpen‘𝑌)) | 
| 60 |  | prdstopn.o | . . 3
⊢ 𝑂 = (TopOpen‘𝑌) | 
| 61 | 59, 60 | eqtr4di 2794 | . 2
⊢ (𝜑 → (TopSet‘𝑌) = 𝑂) | 
| 62 | 61, 10 | eqtr3d 2778 | 1
⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen
∘ 𝑅))) |