This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) ) )