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 ) = (/) ) )