Theorem fitop

Description: A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009)

	Ref	Expression
Assertion	fitop	|- ( J e. Top -> ( fi ` J ) = J )

Proof

Step	Hyp	Ref	Expression
1		inopn	|- ( ( J e. Top /\ x e. J /\ y e. J ) -> ( x i^i y ) e. J )
2	1	3expib	|- ( J e. Top -> ( ( x e. J /\ y e. J ) -> ( x i^i y ) e. J ) )
3	2	ralrimivv	|- ( J e. Top -> A. x e. J A. y e. J ( x i^i y ) e. J )
4		inficl	|- ( J e. Top -> ( A. x e. J A. y e. J ( x i^i y ) e. J <-> ( fi ` J ) = J ) )
5	3 4	mpbid	|- ( J e. Top -> ( fi ` J ) = J )