Theorem clsint2

Description: The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009)

	Ref	Expression
Hypothesis	clsint2.1	|- X = U. J
Assertion	clsint2	|- ( ( J e. Top /\ C C_ ~P X ) -> ( ( cls ` J ) ` |^| C ) C_ |^|_ c e. C ( ( cls ` J ) ` c ) )

Proof

Step	Hyp	Ref	Expression
1		clsint2.1	|- X = U. J
2		sspwuni	|- ( C C_ ~P X <-> U. C C_ X )
3		elssuni	|- ( c e. C -> c C_ U. C )
4		sstr2	|- ( c C_ U. C -> ( U. C C_ X -> c C_ X ) )
5	3 4	syl	|- ( c e. C -> ( U. C C_ X -> c C_ X ) )
6	5	adantl	|- ( ( J e. Top /\ c e. C ) -> ( U. C C_ X -> c C_ X ) )
7		intss1	|- ( c e. C -> |^| C C_ c )
8	1	clsss	|- ( ( J e. Top /\ c C_ X /\ |^| C C_ c ) -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) )
9	7 8	syl3an3	|- ( ( J e. Top /\ c C_ X /\ c e. C ) -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) )
10	9	3com23	|- ( ( J e. Top /\ c e. C /\ c C_ X ) -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) )
11	10	3expia	|- ( ( J e. Top /\ c e. C ) -> ( c C_ X -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) ) )
12	6 11	syld	|- ( ( J e. Top /\ c e. C ) -> ( U. C C_ X -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) ) )
13	12	impancom	|- ( ( J e. Top /\ U. C C_ X ) -> ( c e. C -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) ) )
14	2 13	sylan2b	|- ( ( J e. Top /\ C C_ ~P X ) -> ( c e. C -> ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) ) )
15	14	ralrimiv	|- ( ( J e. Top /\ C C_ ~P X ) -> A. c e. C ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) )
16		ssiin	|- ( ( ( cls ` J ) ` |^| C ) C_ |^|_ c e. C ( ( cls ` J ) ` c ) <-> A. c e. C ( ( cls ` J ) ` |^| C ) C_ ( ( cls ` J ) ` c ) )
17	15 16	sylibr	|- ( ( J e. Top /\ C C_ ~P X ) -> ( ( cls ` J ) ` |^| C ) C_ |^|_ c e. C ( ( cls ` J ) ` c ) )