Theorem pttoponconst

Description: The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypothesis	ptuniconst.2	⊢ 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) )
Assertion	pttoponconst	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ ( 𝑋 ↑m 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ptuniconst.2	⊢ 𝐽 = ( ∏t ‘ ( 𝐴 × { 𝑅 } ) )
2		id	⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
3	2	ralrimivw	⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
4		fconstmpt	⊢ ( 𝐴 × { 𝑅 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
5	4	fveq2i	⊢ ( ∏t ‘ ( 𝐴 × { 𝑅 } ) ) = ( ∏t ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
6	1 5	eqtri	⊢ 𝐽 = ( ∏t ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
7	6	pttopon	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐴 𝑋 ) )
8	3 7	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐴 𝑋 ) )
9		toponmax	⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝑅 )
10		ixpconstg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑅 ) → X 𝑥 ∈ 𝐴 𝑋 = ( 𝑋 ↑m 𝐴 ) )
11	9 10	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → X 𝑥 ∈ 𝐴 𝑋 = ( 𝑋 ↑m 𝐴 ) )
12	11	fveq2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → ( TopOn ‘ X 𝑥 ∈ 𝐴 𝑋 ) = ( TopOn ‘ ( 𝑋 ↑m 𝐴 ) ) )
13	8 12	eleqtrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ ( 𝑋 ↑m 𝐴 ) ) )