Theorem intcld

Description: The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006)

	Ref	Expression
Assertion	intcld	|- ( ( A =/= (/) /\ A C_ ( Clsd ` J ) ) -> |^| A e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		intiin	|- |^| A = |^|_ x e. A x
2		dfss3	|- ( A C_ ( Clsd ` J ) <-> A. x e. A x e. ( Clsd ` J ) )
3		iincld	|- ( ( A =/= (/) /\ A. x e. A x e. ( Clsd ` J ) ) -> |^|_ x e. A x e. ( Clsd ` J ) )
4	2 3	sylan2b	|- ( ( A =/= (/) /\ A C_ ( Clsd ` J ) ) -> |^|_ x e. A x e. ( Clsd ` J ) )
5	1 4	eqeltrid	|- ( ( A =/= (/) /\ A C_ ( Clsd ` J ) ) -> |^| A e. ( Clsd ` J ) )