Metamath Proof Explorer

Theorem pnrmcld

Description: A closed set in a perfectly normal space is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion pnrmcld 
|- ( ( J e. PNrm /\ A e. ( Clsd ` J ) ) -> E. f e. ( J ^m NN ) A = |^| ran f )

Proof

Step Hyp Ref Expression
1 ispnrm 
 |-  ( J e. PNrm <-> ( J e. Nrm /\ ( Clsd ` J ) C_ ran ( f e. ( J ^m NN ) |-> |^| ran f ) ) )
2 1 simprbi 
 |-  ( J e. PNrm -> ( Clsd ` J ) C_ ran ( f e. ( J ^m NN ) |-> |^| ran f ) )
3 2 sselda 
 |-  ( ( J e. PNrm /\ A e. ( Clsd ` J ) ) -> A e. ran ( f e. ( J ^m NN ) |-> |^| ran f ) )
4 eqid 
 |-  ( f e. ( J ^m NN ) |-> |^| ran f ) = ( f e. ( J ^m NN ) |-> |^| ran f )
5 4 elrnmpt 
 |-  ( A e. ( Clsd ` J ) -> ( A e. ran ( f e. ( J ^m NN ) |-> |^| ran f ) <-> E. f e. ( J ^m NN ) A = |^| ran f ) )
6 5 adantl 
 |-  ( ( J e. PNrm /\ A e. ( Clsd ` J ) ) -> ( A e. ran ( f e. ( J ^m NN ) |-> |^| ran f ) <-> E. f e. ( J ^m NN ) A = |^| ran f ) )
7 3 6 mpbid 
 |-  ( ( J e. PNrm /\ A e. ( Clsd ` J ) ) -> E. f e. ( J ^m NN ) A = |^| ran f )