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