ptbasin2

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-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	ptbasin2	$⊢ (A \in V \land F : A ⟶ Top) \to fi (B) = B$

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	ptbasin	$⊢ ((A \in V \land F : A ⟶ Top) \land (u \in B \land v \in B)) \to u \cap v \in B$
3	2	ralrimivva	$⊢ (A \in V \land F : A ⟶ Top) \to \forall u \in B \forall v \in B u \cap v \in B$
4	1	ptuni2	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ B$
5		ixpexg	$⊢ \forall k \in A ⋃ F (k) \in V \to \underset{k \in A}{⨉} ⋃ F (k) \in V$
6		fvex	$⊢ F (k) \in V$
7	6	uniex	$⊢ ⋃ F (k) \in V$
8	7	a1i	$⊢ k \in A \to ⋃ F (k) \in V$
9	5 8	mprg	$⊢ \underset{k \in A}{⨉} ⋃ F (k) \in V$
10	4 9	eqeltrrdi	$⊢ (A \in V \land F : A ⟶ Top) \to ⋃ B \in V$
11		uniexb	$⊢ B \in V \leftrightarrow ⋃ B \in V$
12	10 11	sylibr	$⊢ (A \in V \land F : A ⟶ Top) \to B \in V$
13		inficl	$⊢ B \in V \to (\forall u \in B \forall v \in B u \cap v \in B \leftrightarrow fi (B) = B)$
14	12 13	syl	$⊢ (A \in V \land F : A ⟶ Top) \to (\forall u \in B \forall v \in B u \cap v \in B \leftrightarrow fi (B) = B)$
15	3 14	mpbid	$⊢ (A \in V \land F : A ⟶ Top) \to fi (B) = B$

Metamath Proof Explorer