Metamath Proof Explorer


Theorem nrmsep3

Description: In a normal space, given a closed set B inside an open set A , there is an open set x such that B C_ x C_ cls ( x ) C_ A . (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion nrmsep3
|- ( ( J e. Nrm /\ ( A e. J /\ B e. ( Clsd ` J ) /\ B C_ A ) ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) )

Proof

Step Hyp Ref Expression
1 isnrm
 |-  ( J e. Nrm <-> ( J e. Top /\ A. y e. J A. z e. ( ( Clsd ` J ) i^i ~P y ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) ) )
2 pweq
 |-  ( y = A -> ~P y = ~P A )
3 2 ineq2d
 |-  ( y = A -> ( ( Clsd ` J ) i^i ~P y ) = ( ( Clsd ` J ) i^i ~P A ) )
4 sseq2
 |-  ( y = A -> ( ( ( cls ` J ) ` x ) C_ y <-> ( ( cls ` J ) ` x ) C_ A ) )
5 4 anbi2d
 |-  ( y = A -> ( ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) <-> ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
6 5 rexbidv
 |-  ( y = A -> ( E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) <-> E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
7 3 6 raleqbidv
 |-  ( y = A -> ( A. z e. ( ( Clsd ` J ) i^i ~P y ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) <-> A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
8 7 rspccv
 |-  ( A. y e. J A. z e. ( ( Clsd ` J ) i^i ~P y ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) -> ( A e. J -> A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
9 1 8 simplbiim
 |-  ( J e. Nrm -> ( A e. J -> A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
10 elin
 |-  ( B e. ( ( Clsd ` J ) i^i ~P A ) <-> ( B e. ( Clsd ` J ) /\ B e. ~P A ) )
11 elpwg
 |-  ( B e. ( Clsd ` J ) -> ( B e. ~P A <-> B C_ A ) )
12 11 pm5.32i
 |-  ( ( B e. ( Clsd ` J ) /\ B e. ~P A ) <-> ( B e. ( Clsd ` J ) /\ B C_ A ) )
13 10 12 bitri
 |-  ( B e. ( ( Clsd ` J ) i^i ~P A ) <-> ( B e. ( Clsd ` J ) /\ B C_ A ) )
14 cleq1lem
 |-  ( z = B -> ( ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) <-> ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
15 14 rexbidv
 |-  ( z = B -> ( E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) <-> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
16 15 rspccv
 |-  ( A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) -> ( B e. ( ( Clsd ` J ) i^i ~P A ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
17 13 16 syl5bir
 |-  ( A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) -> ( ( B e. ( Clsd ` J ) /\ B C_ A ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) )
18 9 17 syl6
 |-  ( J e. Nrm -> ( A e. J -> ( ( B e. ( Clsd ` J ) /\ B C_ A ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) )
19 18 exp4a
 |-  ( J e. Nrm -> ( A e. J -> ( B e. ( Clsd ` J ) -> ( B C_ A -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) ) )
20 19 3imp2
 |-  ( ( J e. Nrm /\ ( A e. J /\ B e. ( Clsd ` J ) /\ B C_ A ) ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) )