Theorem topmtcl

Description: The meet of a collection of topologies on X is again a topology on X . (Contributed by Jeff Hankins, 5-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	topmtcl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ ( TopOn ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		toponmre	⊢ ( 𝑋 ∈ 𝑉 → ( TopOn ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )
2		mrerintcl	⊢ ( ( ( TopOn ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ ( TopOn ‘ 𝑋 ) )
3	1 2	sylan	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑆 ⊆ ( TopOn ‘ 𝑋 ) ) → ( 𝒫 𝑋 ∩ ∩ 𝑆 ) ∈ ( TopOn ‘ 𝑋 ) )