Metamath Proof Explorer

Theorem prdstps

Description: A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses prdstopn.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdstopn.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdstopn.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdstps.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ TopSp )
Assertion prdstps ( 𝜑 → 𝑌 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 prdstopn.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdstopn.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3 prdstopn.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4 prdstps.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ TopSp )
5 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ TopSp )
6 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
7 eqid ⊢ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) )
8 6 7 istps ⊢ ( ( 𝑅 ‘ 𝑥 ) ∈ TopSp ↔ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ( TopOn ‘ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
9 5 8 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ( TopOn ‘ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
10 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ( TopOn ‘ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
11 eqid ⊢ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
12 11 pttopon ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ∀ 𝑥 ∈ 𝐼 ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ( TopOn ‘ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) ∈ ( TopOn ‘ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
13 3 10 12 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) ∈ ( TopOn ‘ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
14 4 3 fexd ⊢ ( 𝜑 → 𝑅 ∈ V )
15 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
16 4 fdmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
17 eqid ⊢ ( TopSet ‘ 𝑌 ) = ( TopSet ‘ 𝑌 )
18 1 2 14 15 16 17 prdstset ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
19 topnfn ⊢ TopOpen Fn V
20 dffn2 ⊢ ( TopOpen Fn V ↔ TopOpen : V ⟶ V )
21 19 20 mpbi ⊢ TopOpen : V ⟶ V
22 ssv ⊢ TopSp ⊆ V
23 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ TopSp ∧ TopSp ⊆ V ) → 𝑅 : 𝐼 ⟶ V )
24 4 22 23 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ V )
25 fcompt ⊢ ( ( TopOpen : V ⟶ V ∧ 𝑅 : 𝐼 ⟶ V ) → ( TopOpen ∘ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
26 21 24 25 sylancr ⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
27 26 fveq2d ⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) )
28 18 27 eqtrd ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) )
29 1 2 14 15 16 prdsbas ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
30 29 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ ( Base ‘ 𝑌 ) ) = ( TopOn ‘ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
31 13 28 30 3eltr4d ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
32 15 17 tsettps ⊢ ( ( TopSet ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) → 𝑌 ∈ TopSp )
33 31 32 syl ⊢ ( 𝜑 → 𝑌 ∈ TopSp )