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 biimtrrid 
 |-  ( 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 ) )