Theorem fitop

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

	Ref	Expression
Assertion	fitop	⊢ ( 𝐽 ∈ Top → ( fi ‘ 𝐽 ) = 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		inopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
2	1	3expib	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ) )
3	2	ralrimivv	⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
4		inficl	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ↔ ( fi ‘ 𝐽 ) = 𝐽 ) )
5	3 4	mpbid	⊢ ( 𝐽 ∈ Top → ( fi ‘ 𝐽 ) = 𝐽 )