Metamath Proof Explorer

Theorem ptbas

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

		Ref	Expression
	Hypothesis	ptbas.1	$⊢ B = \{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))\}$
	Assertion	ptbas	$⊢ (A \in V \land F : A ⟶ Top) \to B \in TopBases$

Step	Hyp	Ref	Expression
1		ptbas.1	$⊢ B = \{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))\}$
2	1	ptbasin2	$⊢ (A \in V \land F : A ⟶ Top) \to fi (B) = B$
3		fibas	$⊢ fi (B) \in TopBases$
4	2 3	eqeltrrdi	$⊢ (A \in V \land F : A ⟶ Top) \to B \in TopBases$