Metamath Proof Explorer

Theorem ispnrm

Description: The property of being perfectly normal. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ispnrm 
|- ( J e. PNrm <-> ( J e. Nrm /\ ( Clsd ` J ) C_ ran ( f e. ( J ^m NN ) |-> |^| ran f ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( j = J -> ( Clsd ` j ) = ( Clsd ` J ) )
2 oveq1 
 |-  ( j = J -> ( j ^m NN ) = ( J ^m NN ) )
3 2 mpteq1d 
 |-  ( j = J -> ( f e. ( j ^m NN ) |-> |^| ran f ) = ( f e. ( J ^m NN ) |-> |^| ran f ) )
4 3 rneqd 
 |-  ( j = J -> ran ( f e. ( j ^m NN ) |-> |^| ran f ) = ran ( f e. ( J ^m NN ) |-> |^| ran f ) )
5 1 4 sseq12d 
 |-  ( j = J -> ( ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) <-> ( Clsd ` J ) C_ ran ( f e. ( J ^m NN ) |-> |^| ran f ) ) )
6 df-pnrm 
 |-  PNrm = { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }
7 5 6 elrab2 
 |-  ( J e. PNrm <-> ( J e. Nrm /\ ( Clsd ` J ) C_ ran ( f e. ( J ^m NN ) |-> |^| ran f ) ) )