Theorem clsndisj

Description: Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of Munkres p. 95. (Contributed by NM, 26-Feb-2007)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	clsndisj	|- ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2		simp1	|- ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> J e. Top )
3		simp2	|- ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> S C_ X )
4	1	clsss3	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
5	4	sseld	|- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) -> P e. X ) )
6	5	3impia	|- ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> P e. X )
7		simp3	|- ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> P e. ( ( cls ` J ) ` S ) )
8	1	elcls	|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) )
9	8	biimpa	|- ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ P e. ( ( cls ` J ) ` S ) ) -> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) )
10	2 3 6 7 9	syl31anc	|- ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) -> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) )
11		eleq2	|- ( x = U -> ( P e. x <-> P e. U ) )
12		ineq1	|- ( x = U -> ( x i^i S ) = ( U i^i S ) )
13	12	neeq1d	|- ( x = U -> ( ( x i^i S ) =/= (/) <-> ( U i^i S ) =/= (/) ) )
14	11 13	imbi12d	|- ( x = U -> ( ( P e. x -> ( x i^i S ) =/= (/) ) <-> ( P e. U -> ( U i^i S ) =/= (/) ) ) )
15	14	rspccv	|- ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( U e. J -> ( P e. U -> ( U i^i S ) =/= (/) ) ) )
16	15	imp32	|- ( ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )
17	10 16	sylan	|- ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )