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