Theorem 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 | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
Assertion	ptbasin2	|- ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = B )

Proof

Step	Hyp	Ref	Expression
1		ptbas.1	|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) }
2	1	ptbasin	|- ( ( ( A e. V /\ F : A --> Top ) /\ ( u e. B /\ v e. B ) ) -> ( u i^i v ) e. B )
3	2	ralrimivva	|- ( ( A e. V /\ F : A --> Top ) -> A. u e. B A. v e. B ( u i^i v ) e. B )
4	1	ptuni2	|- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. B )
5		ixpexg	|- ( A. k e. A U. ( F ` k ) e. _V -> X_ k e. A U. ( F ` k ) e. _V )
6		fvex	|- ( F ` k ) e. _V
7	6	uniex	|- U. ( F ` k ) e. _V
8	7	a1i	|- ( k e. A -> U. ( F ` k ) e. _V )
9	5 8	mprg	|- X_ k e. A U. ( F ` k ) e. _V
10	4 9	eqeltrrdi	|- ( ( A e. V /\ F : A --> Top ) -> U. B e. _V )
11		uniexb	|- ( B e. _V <-> U. B e. _V )
12	10 11	sylibr	|- ( ( A e. V /\ F : A --> Top ) -> B e. _V )
13		inficl	|- ( B e. _V -> ( A. u e. B A. v e. B ( u i^i v ) e. B <-> ( fi ` B ) = B ) )
14	12 13	syl	|- ( ( A e. V /\ F : A --> Top ) -> ( A. u e. B A. v e. B ( u i^i v ) e. B <-> ( fi ` B ) = B ) )
15	3 14	mpbid	|- ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = B )