Metamath Proof Explorer

Theorem nrmsep

Description: In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010)

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

Proof

Step Hyp Ref Expression
1 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
2 1 ad2antrr 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> J e. Top )
3 elssuni 
 |-  ( x e. J -> x C_ U. J )
4 3 ad2antrl 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> x C_ U. J )
5 eqid 
 |-  U. J = U. J
6 5 clscld 
 |-  ( ( J e. Top /\ x C_ U. J ) -> ( ( cls ` J ) ` x ) e. ( Clsd ` J ) )
7 2 4 6 syl2anc 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( ( cls ` J ) ` x ) e. ( Clsd ` J ) )
8 5 cldopn 
 |-  ( ( ( cls ` J ) ` x ) e. ( Clsd ` J ) -> ( U. J \ ( ( cls ` J ) ` x ) ) e. J )
9 7 8 syl 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( U. J \ ( ( cls ` J ) ` x ) ) e. J )
10 simprrl 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> C C_ x )
11 incom 
 |-  ( D i^i ( ( cls ` J ) ` x ) ) = ( ( ( cls ` J ) ` x ) i^i D )
12 simprrr 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( ( ( cls ` J ) ` x ) i^i D ) = (/) )
13 11 12 eqtrid 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( D i^i ( ( cls ` J ) ` x ) ) = (/) )
14 simplr2 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> D e. ( Clsd ` J ) )
15 5 cldss 
 |-  ( D e. ( Clsd ` J ) -> D C_ U. J )
16 reldisj 
 |-  ( D C_ U. J -> ( ( D i^i ( ( cls ` J ) ` x ) ) = (/) <-> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) )
17 14 15 16 3syl 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( ( D i^i ( ( cls ` J ) ` x ) ) = (/) <-> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) )
18 13 17 mpbid 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) )
19 5 sscls 
 |-  ( ( J e. Top /\ x C_ U. J ) -> x C_ ( ( cls ` J ) ` x ) )
20 2 4 19 syl2anc 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> x C_ ( ( cls ` J ) ` x ) )
21 20 ssrind 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) C_ ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) )
22 disjdif 
 |-  ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/)
23 sseq0 
 |-  ( ( ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) C_ ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) /\ ( ( ( cls ` J ) ` x ) i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) -> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) )
24 21 22 23 sylancl 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) )
25 sseq2 
 |-  ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( D C_ y <-> D C_ ( U. J \ ( ( cls ` J ) ` x ) ) ) )
26 ineq2 
 |-  ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( x i^i y ) = ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) )
27 26 eqeq1d 
 |-  ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( ( x i^i y ) = (/) <-> ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) )
28 25 27 3anbi23d 
 |-  ( y = ( U. J \ ( ( cls ` J ) ` x ) ) -> ( ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) <-> ( C C_ x /\ D C_ ( U. J \ ( ( cls ` J ) ` x ) ) /\ ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) ) )
29 28 rspcev 
 |-  ( ( ( U. J \ ( ( cls ` J ) ` x ) ) e. J /\ ( C C_ x /\ D C_ ( U. J \ ( ( cls ` J ) ` x ) ) /\ ( x i^i ( U. J \ ( ( cls ` J ) ` x ) ) ) = (/) ) ) -> E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) )
30 9 10 18 24 29 syl13anc 
 |-  ( ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) /\ ( x e. J /\ ( C C_ x /\ ( ( ( cls ` J ) ` x ) i^i D ) = (/) ) ) ) -> E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) )
31 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 ) = (/) ) )
32 30 31 reximddv 
 |-  ( ( J e. Nrm /\ ( C e. ( Clsd ` J ) /\ D e. ( Clsd ` J ) /\ ( C i^i D ) = (/) ) ) -> E. x e. J E. y e. J ( C C_ x /\ D C_ y /\ ( x i^i y ) = (/) ) )