Metamath Proof Explorer

Theorem pttop

Description: The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015)

		Ref	Expression
	Assertion	pttop	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) \in Top$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ Top \to F Fn A$
2		eqid	$⊢ \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} = \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}$
3	2	ptval	$⊢ (A \in V \land F Fn A) \to \prod_{𝑡} (F) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
4	1 3	sylan2	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) = topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\})$
5	2	ptbas	$⊢ (A \in V \land F : A ⟶ Top) \to \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases$
6		tgcl	$⊢ \{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\} \in TopBases \to topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}) \in Top$
7	5 6	syl	$⊢ (A \in V \land F : A ⟶ Top) \to topGen (\{x \| \exists g ((g Fn A \land \forall y \in A g (y) \in F (y) \land \exists z \in Fin \forall y \in (A ∖ z) g (y) = ⋃ F (y)) \land x = \underset{y \in A}{⨉} g (y))\}) \in Top$
8	4 7	eqeltrd	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) \in Top$