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 𝑥 ∈ 𝐴 𝐵 ) )