This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fitop

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

		Ref	Expression
	Assertion	fitop	$⊢ J \in Top \to fi (J) = J$

Step	Hyp	Ref	Expression
1		inopn	$⊢ (J \in Top \land x \in J \land y \in J) \to x \cap y \in J$
2	1	3expib	$⊢ J \in Top \to ((x \in J \land y \in J) \to x \cap y \in J)$
3	2	ralrimivv	$⊢ J \in Top \to \forall x \in J \forall y \in J x \cap y \in J$
4		inficl	$⊢ J \in Top \to (\forall x \in J \forall y \in J x \cap y \in J \leftrightarrow fi (J) = J)$
5	3 4	mpbid	$⊢ J \in Top \to fi (J) = J$