Metamath Proof Explorer

Theorem nrmsep2

Description: In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion nrmsep2 
|- ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> E. x e. J ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> J e. Nrm )
2 simpr2 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> D e. ( Clsd ` J ) )
3 eqid 
 |-  U. J = U. J
4 3 cldopn 
 |-  ( D e. ( Clsd ` J ) -> ( U. J \ D ) e. J )
5 2 4 syl 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> ( U. J \ D ) e. J )
6 simpr1 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> C e. ( Clsd ` J ) )
7 simpr3 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> ( C i^i D ) = (/) )
8 3 cldss 
 |-  ( C e. ( Clsd ` J ) -> C C_ U. J )
9 reldisj 
 |-  ( C C_ U. J -> ( ( C i^i D ) = (/) <-> C C_ ( U. J \ D ) ) )
10 6 8 9 3syl 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> ( ( C i^i D ) = (/) <-> C C_ ( U. J \ D ) ) )
11 7 10 mpbid 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> C C_ ( U. J \ D ) )
12 nrmsep3 
 |-  ( ( J e. Nrm /\ ( ( U. J \ D ) e. J /\ C e. ( Clsd ` J ) /\ C C_ ( U. J \ D ) ) ) -> E. x e. J ( C C_ x /\ ( ( cls ` J ) ` x ) C_ ( U. J \ D ) ) )
13 1 5 6 11 12 syl13anc 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> E. x e. J ( C C_ x /\ ( ( cls ` J ) ` x ) C_ ( U. J \ D ) ) )
14 ssdifin0 
 |-  ( ( ( cls ` J ) ` x ) C_ ( U. J \ D ) -> ( ( ( cls ` J ) ` x ) i^i D ) = (/) )
15 14 anim2i 
 |-  ( ( C C_ x /\ ( ( cls ` J ) ` x ) C_ ( U. J \ D ) ) -> ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) )
16 15 reximi 
 |-  ( E. x e. J ( C C_ x /\ ( ( cls ` J ) ` x ) C_ ( U. J \ D ) ) -> E. x e. J ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) )
17 13 16 syl 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> E. x e. J ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) )