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 𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽 )