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 | 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	ptbas	|- ( ( A e. V /\ F : A --> Top ) -> B e. TopBases )

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	ptbasin2	|- ( ( A e. V /\ F : A --> Top ) -> ( fi ` B ) = B )
3		fibas	|- ( fi ` B ) e. TopBases
4	2 3	eqeltrrdi	|- ( ( A e. V /\ F : A --> Top ) -> B e. TopBases )