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 fex ⊢ ( ( 𝑅 : 𝐼 ⟶ TopSp ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
15 4 3 14 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ V )
16 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
17 4 fdmd ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
18 eqid ⊢ ( TopSet ‘ 𝑌 ) = ( TopSet ‘ 𝑌 )
19 1 2 15 16 17 18 prdstset ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) )
20 topnfn ⊢ TopOpen Fn V
21 dffn2 ⊢ ( TopOpen Fn V ↔ TopOpen : V ⟶ V )
22 20 21 mpbi ⊢ TopOpen : V ⟶ V
23 ssv ⊢ TopSp ⊆ V
24 fss ⊢ ( ( 𝑅 : 𝐼 ⟶ TopSp ∧ TopSp ⊆ V ) → 𝑅 : 𝐼 ⟶ V )
25 4 23 24 sylancl ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ V )
26 fcompt ⊢ ( ( TopOpen : V ⟶ V ∧ 𝑅 : 𝐼 ⟶ V ) → ( TopOpen ∘ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
27 22 25 26 sylancr ⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
28 27 fveq2d ⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) )
29 19 28 eqtrd ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( TopOpen ‘ ( 𝑅 ‘ 𝑥 ) ) ) ) )
30 1 2 15 16 17 prdsbas ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
31 30 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ ( Base ‘ 𝑌 ) ) = ( TopOn ‘ X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) )
32 13 29 31 3eltr4d ⊢ ( 𝜑 → ( TopSet ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) )
33 16 18 tsettps ⊢ ( ( TopSet ‘ 𝑌 ) ∈ ( TopOn ‘ ( Base ‘ 𝑌 ) ) → 𝑌 ∈ TopSp )
34 32 33 syl ⊢ ( 𝜑 → 𝑌 ∈ TopSp )