| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prdstmdd.y | . . 3
⊢ 𝑌 = (𝑆Xs𝑅) | 
| 2 |  | prdstmdd.i | . . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 3 |  | prdstmdd.s | . . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) | 
| 4 |  | prdstmdd.r | . . . 4
⊢ (𝜑 → 𝑅:𝐼⟶TopMnd) | 
| 5 |  | tmdmnd 24083 | . . . . 5
⊢ (𝑥 ∈ TopMnd → 𝑥 ∈ Mnd) | 
| 6 | 5 | ssriv 3987 | . . . 4
⊢ TopMnd
⊆ Mnd | 
| 7 |  | fss 6752 | . . . 4
⊢ ((𝑅:𝐼⟶TopMnd ∧ TopMnd ⊆ Mnd)
→ 𝑅:𝐼⟶Mnd) | 
| 8 | 4, 6, 7 | sylancl 586 | . . 3
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) | 
| 9 | 1, 2, 3, 8 | prdsmndd 18783 | . 2
⊢ (𝜑 → 𝑌 ∈ Mnd) | 
| 10 |  | tmdtps 24084 | . . . . 5
⊢ (𝑥 ∈ TopMnd → 𝑥 ∈ TopSp) | 
| 11 | 10 | ssriv 3987 | . . . 4
⊢ TopMnd
⊆ TopSp | 
| 12 |  | fss 6752 | . . . 4
⊢ ((𝑅:𝐼⟶TopMnd ∧ TopMnd ⊆ TopSp)
→ 𝑅:𝐼⟶TopSp) | 
| 13 | 4, 11, 12 | sylancl 586 | . . 3
⊢ (𝜑 → 𝑅:𝐼⟶TopSp) | 
| 14 | 1, 3, 2, 13 | prdstps 23637 | . 2
⊢ (𝜑 → 𝑌 ∈ TopSp) | 
| 15 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 16 | 3 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑆 ∈ 𝑉) | 
| 17 | 2 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝐼 ∈ 𝑊) | 
| 18 | 4 | ffnd 6737 | . . . . . . . 8
⊢ (𝜑 → 𝑅 Fn 𝐼) | 
| 19 | 18 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑅 Fn 𝐼) | 
| 20 |  | simp2 1138 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑓 ∈ (Base‘𝑌)) | 
| 21 |  | simp3 1139 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → 𝑔 ∈ (Base‘𝑌)) | 
| 22 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝑌) = (+g‘𝑌) | 
| 23 | 1, 15, 16, 17, 19, 20, 21, 22 | prdsplusgval 17518 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (Base‘𝑌) ∧ 𝑔 ∈ (Base‘𝑌)) → (𝑓(+g‘𝑌)𝑔) = (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) | 
| 24 | 23 | mpoeq3dva 7510 | . . . . 5
⊢ (𝜑 → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓(+g‘𝑌)𝑔)) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))))) | 
| 25 |  | eqid 2737 | . . . . . 6
⊢
(+𝑓‘𝑌) = (+𝑓‘𝑌) | 
| 26 | 15, 22, 25 | plusffval 18659 | . . . . 5
⊢
(+𝑓‘𝑌) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓(+g‘𝑌)𝑔)) | 
| 27 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑓 ∈ V | 
| 28 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑔 ∈ V | 
| 29 | 27, 28 | op1std 8024 | . . . . . . . . 9
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (1st ‘𝑧) = 𝑓) | 
| 30 | 29 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑔〉 → ((1st ‘𝑧)‘𝑘) = (𝑓‘𝑘)) | 
| 31 | 27, 28 | op2ndd 8025 | . . . . . . . . 9
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (2nd ‘𝑧) = 𝑔) | 
| 32 | 31 | fveq1d 6908 | . . . . . . . 8
⊢ (𝑧 = 〈𝑓, 𝑔〉 → ((2nd ‘𝑧)‘𝑘) = (𝑔‘𝑘)) | 
| 33 | 30, 32 | oveq12d 7449 | . . . . . . 7
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)) = ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) | 
| 34 | 33 | mpteq2dv 5244 | . . . . . 6
⊢ (𝑧 = 〈𝑓, 𝑔〉 → (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) = (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) | 
| 35 | 34 | mpompt 7547 | . . . . 5
⊢ (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)))) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑘 ∈ 𝐼 ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘)))) | 
| 36 | 24, 26, 35 | 3eqtr4g 2802 | . . . 4
⊢ (𝜑 →
(+𝑓‘𝑌) = (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))))) | 
| 37 |  | eqid 2737 | . . . . 5
⊢
(∏t‘(TopOpen ∘ 𝑅)) = (∏t‘(TopOpen
∘ 𝑅)) | 
| 38 |  | eqid 2737 | . . . . . . . 8
⊢
(TopOpen‘𝑌) =
(TopOpen‘𝑌) | 
| 39 | 15, 38 | istps 22940 | . . . . . . 7
⊢ (𝑌 ∈ TopSp ↔
(TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) | 
| 40 | 14, 39 | sylib 218 | . . . . . 6
⊢ (𝜑 → (TopOpen‘𝑌) ∈
(TopOn‘(Base‘𝑌))) | 
| 41 |  | txtopon 23599 | . . . . . 6
⊢
(((TopOpen‘𝑌)
∈ (TopOn‘(Base‘𝑌)) ∧ (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) → ((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) ∈
(TopOn‘((Base‘𝑌) × (Base‘𝑌)))) | 
| 42 | 40, 40, 41 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) ∈
(TopOn‘((Base‘𝑌) × (Base‘𝑌)))) | 
| 43 |  | topnfn 17470 | . . . . . . . 8
⊢ TopOpen
Fn V | 
| 44 |  | ssv 4008 | . . . . . . . 8
⊢ TopSp
⊆ V | 
| 45 |  | fnssres 6691 | . . . . . . . 8
⊢ ((TopOpen
Fn V ∧ TopSp ⊆ V) → (TopOpen ↾ TopSp) Fn
TopSp) | 
| 46 | 43, 44, 45 | mp2an 692 | . . . . . . 7
⊢ (TopOpen
↾ TopSp) Fn TopSp | 
| 47 |  | fvres 6925 | . . . . . . . . 9
⊢ (𝑥 ∈ TopSp → ((TopOpen
↾ TopSp)‘𝑥) =
(TopOpen‘𝑥)) | 
| 48 |  | eqid 2737 | . . . . . . . . . 10
⊢
(TopOpen‘𝑥) =
(TopOpen‘𝑥) | 
| 49 | 48 | tpstop 22943 | . . . . . . . . 9
⊢ (𝑥 ∈ TopSp →
(TopOpen‘𝑥) ∈
Top) | 
| 50 | 47, 49 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝑥 ∈ TopSp → ((TopOpen
↾ TopSp)‘𝑥)
∈ Top) | 
| 51 | 50 | rgen 3063 | . . . . . . 7
⊢
∀𝑥 ∈
TopSp ((TopOpen ↾ TopSp)‘𝑥) ∈ Top | 
| 52 |  | ffnfv 7139 | . . . . . . 7
⊢ ((TopOpen
↾ TopSp):TopSp⟶Top ↔ ((TopOpen ↾ TopSp) Fn TopSp ∧
∀𝑥 ∈ TopSp
((TopOpen ↾ TopSp)‘𝑥) ∈ Top)) | 
| 53 | 46, 51, 52 | mpbir2an 711 | . . . . . 6
⊢ (TopOpen
↾ TopSp):TopSp⟶Top | 
| 54 |  | fco2 6762 | . . . . . 6
⊢
(((TopOpen ↾ TopSp):TopSp⟶Top ∧ 𝑅:𝐼⟶TopSp) → (TopOpen ∘ 𝑅):𝐼⟶Top) | 
| 55 | 53, 13, 54 | sylancr 587 | . . . . 5
⊢ (𝜑 → (TopOpen ∘ 𝑅):𝐼⟶Top) | 
| 56 | 33 | mpompt 7547 | . . . . . 6
⊢ (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (((1st
‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) = (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) | 
| 57 |  | eqid 2737 | . . . . . . . 8
⊢
(TopOpen‘(𝑅‘𝑘)) = (TopOpen‘(𝑅‘𝑘)) | 
| 58 |  | eqid 2737 | . . . . . . . 8
⊢
(+g‘(𝑅‘𝑘)) = (+g‘(𝑅‘𝑘)) | 
| 59 | 4 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ TopMnd) | 
| 60 | 40 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen‘𝑌) ∈ (TopOn‘(Base‘𝑌))) | 
| 61 | 60, 60 | cnmpt1st 23676 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ 𝑓) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) | 
| 62 | 1, 3, 2, 18, 38 | prdstopn 23636 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (TopOpen‘𝑌) =
(∏t‘(TopOpen ∘ 𝑅))) | 
| 63 | 62 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen‘𝑌) = (∏t‘(TopOpen
∘ 𝑅))) | 
| 64 | 63, 60 | eqeltrrd 2842 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) ∈
(TopOn‘(Base‘𝑌))) | 
| 65 |  | toponuni 22920 | . . . . . . . . . . . . 13
⊢
((∏t‘(TopOpen ∘ 𝑅)) ∈ (TopOn‘(Base‘𝑌)) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) | 
| 66 | 64, 65 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (Base‘𝑌) = ∪
(∏t‘(TopOpen ∘ 𝑅))) | 
| 67 | 66 | mpteq1d 5237 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) = (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘))) | 
| 68 | 2 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐼 ∈ 𝑊) | 
| 69 | 55 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (TopOpen ∘ 𝑅):𝐼⟶Top) | 
| 70 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) | 
| 71 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ ∪ (∏t‘(TopOpen ∘ 𝑅)) = ∪ (∏t‘(TopOpen ∘ 𝑅)) | 
| 72 | 71, 37 | ptpjcn 23619 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑊 ∧ (TopOpen ∘ 𝑅):𝐼⟶Top ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) | 
| 73 | 68, 69, 70, 72 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ ∪
(∏t‘(TopOpen ∘ 𝑅)) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) | 
| 74 | 67, 73 | eqeltrd 2841 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) ∈ ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘))) | 
| 75 | 63 | eqcomd 2743 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∏t‘(TopOpen
∘ 𝑅)) =
(TopOpen‘𝑌)) | 
| 76 |  | fvco3 7008 | . . . . . . . . . . . 12
⊢ ((𝑅:𝐼⟶TopMnd ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) | 
| 77 | 4, 76 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((TopOpen ∘ 𝑅)‘𝑘) = (TopOpen‘(𝑅‘𝑘))) | 
| 78 | 75, 77 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((∏t‘(TopOpen
∘ 𝑅)) Cn ((TopOpen
∘ 𝑅)‘𝑘)) = ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑘)))) | 
| 79 | 74, 78 | eleqtrd 2843 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ (Base‘𝑌) ↦ (𝑥‘𝑘)) ∈ ((TopOpen‘𝑌) Cn (TopOpen‘(𝑅‘𝑘)))) | 
| 80 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑥 = 𝑓 → (𝑥‘𝑘) = (𝑓‘𝑘)) | 
| 81 | 60, 60, 61, 60, 79, 80 | cnmpt21 23679 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑓‘𝑘)) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) | 
| 82 | 60, 60 | cnmpt2nd 23677 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ 𝑔) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) | 
| 83 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑥 = 𝑔 → (𝑥‘𝑘) = (𝑔‘𝑘)) | 
| 84 | 60, 60, 82, 60, 79, 83 | cnmpt21 23679 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ (𝑔‘𝑘)) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) | 
| 85 | 57, 58, 59, 60, 60, 81, 84 | cnmpt2plusg 24096 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) | 
| 86 | 77 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘)) = (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘(𝑅‘𝑘)))) | 
| 87 | 85, 86 | eleqtrrd 2844 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑓 ∈ (Base‘𝑌), 𝑔 ∈ (Base‘𝑌) ↦ ((𝑓‘𝑘)(+g‘(𝑅‘𝑘))(𝑔‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘))) | 
| 88 | 56, 87 | eqeltrid 2845 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘))) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn ((TopOpen ∘ 𝑅)‘𝑘))) | 
| 89 | 37, 42, 2, 55, 88 | ptcn 23635 | . . . 4
⊢ (𝜑 → (𝑧 ∈ ((Base‘𝑌) × (Base‘𝑌)) ↦ (𝑘 ∈ 𝐼 ↦ (((1st ‘𝑧)‘𝑘)(+g‘(𝑅‘𝑘))((2nd ‘𝑧)‘𝑘)))) ∈ (((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) Cn
(∏t‘(TopOpen ∘ 𝑅)))) | 
| 90 | 36, 89 | eqeltrd 2841 | . . 3
⊢ (𝜑 →
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn
(∏t‘(TopOpen ∘ 𝑅)))) | 
| 91 | 62 | oveq2d 7447 | . . 3
⊢ (𝜑 → (((TopOpen‘𝑌) ×t
(TopOpen‘𝑌)) Cn
(TopOpen‘𝑌)) =
(((TopOpen‘𝑌)
×t (TopOpen‘𝑌)) Cn (∏t‘(TopOpen
∘ 𝑅)))) | 
| 92 | 90, 91 | eleqtrrd 2844 | . 2
⊢ (𝜑 →
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌))) | 
| 93 | 25, 38 | istmd 24082 | . 2
⊢ (𝑌 ∈ TopMnd ↔ (𝑌 ∈ Mnd ∧ 𝑌 ∈ TopSp ∧
(+𝑓‘𝑌) ∈ (((TopOpen‘𝑌) ×t (TopOpen‘𝑌)) Cn (TopOpen‘𝑌)))) | 
| 94 | 9, 14, 92, 93 | syl3anbrc 1344 | 1
⊢ (𝜑 → 𝑌 ∈ TopMnd) |