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

Metamath Proof Explorer

Theorem ptunimpt

Description: Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 ptunimpt.j ⊢ 𝐽 = ( ∏t ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) )
2 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐾 )
3 2 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐾 ∈ Top ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) = 𝐾 )
4 3 eqcomd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐾 ∈ Top ) → 𝐾 = ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
5 4 unieqd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐾 ∈ Top ) → ∪ 𝐾 = ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
6 5 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top → ∀ 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ) → ∀ 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
8 ixpeq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) → X 𝑥 ∈ 𝐴 ∪ 𝐾 = X 𝑥 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ) → X 𝑥 ∈ 𝐴 ∪ 𝐾 = X 𝑥 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
10 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 )
11 10 nfuni ⊢ Ⅎ 𝑥 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 )
12 nfcv ⊢ Ⅎ 𝑦 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 )
13 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
14 13 unieqd ⊢ ( 𝑦 = 𝑥 → ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 ) = ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 ) )
15 11 12 14 cbvixp ⊢ X 𝑦 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 ) = X 𝑥 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑥 )
16 9 15 eqtr4di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ) → X 𝑥 ∈ 𝐴 ∪ 𝐾 = X 𝑦 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 ) )
17 2 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) : 𝐴 ⟶ Top )
18 1 ptuni ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) : 𝐴 ⟶ Top ) → X 𝑦 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 ) = ∪ 𝐽 )
19 17 18 sylan2b ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ) → X 𝑦 ∈ 𝐴 ∪ ( ( 𝑥 ∈ 𝐴 ↦ 𝐾 ) ‘ 𝑦 ) = ∪ 𝐽 )
20 16 19 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐾 ∈ Top ) → X 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽 )