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

Metamath Proof Explorer

Theorem pttopon

Description: The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis ptunimpt.j ⊢ 𝐽 = ( ∏t ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) )
Assertion pttopon ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐴 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ptunimpt.j ⊢ 𝐽 = ( ∏t ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) )
2 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) → 𝐾 ∈ Top )
3 2 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top )
4 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐾 )
5 4 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) : 𝐴 ⟶ Top )
6 3 5 sylib ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) : 𝐴 ⟶ Top )
7 pttop ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) : 𝐴 ⟶ Top ) → ( ∏t ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ) ∈ Top )
8 1 7 eqeltrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) : 𝐴 ⟶ Top ) → 𝐽 ∈ Top )
9 6 8 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → 𝐽 ∈ Top )
10 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐾 )
11 10 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝐾 )
12 ixpeq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝐾 → X 𝑥 ∈ 𝐴 𝐵 = X 𝑥 ∈ 𝐴 ∪ 𝐾 )
13 11 12 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) → X 𝑥 ∈ 𝐴 𝐵 = X 𝑥 ∈ 𝐴 ∪ 𝐾 )
14 13 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → X 𝑥 ∈ 𝐴 𝐵 = X 𝑥 ∈ 𝐴 ∪ 𝐾 )
15 1 ptunimpt ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ) → X 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽 )
16 3 15 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → X 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽 )
17 14 16 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → X 𝑥 ∈ 𝐴 𝐵 = ∪ 𝐽 )
18 istopon ⊢ ( 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝐽 ∈ Top ∧ X 𝑥 ∈ 𝐴 𝐵 = ∪ 𝐽 ) )
19 9 17 18 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ ( TopOn ‘ 𝐵 ) ) → 𝐽 ∈ ( TopOn ‘ X 𝑥 ∈ 𝐴 𝐵 ) )