Metamath Proof Explorer

Theorem iscnrm2

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

Ref Expression
Assertion iscnrm2 
|- ( J e. ( TopOn ` X ) -> ( J e. CNrm <-> A. x e. ~P X ( J |`t x ) e. Nrm ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 iscnrm 
 |-  ( J e. CNrm <-> ( J e. Top /\ A. x e. ~P U. J ( J |`t x ) e. Nrm ) )
4 3 baib 
 |-  ( J e. Top -> ( J e. CNrm <-> A. x e. ~P U. J ( J |`t x ) e. Nrm ) )
5 1 4 syl 
 |-  ( J e. ( TopOn ` X ) -> ( J e. CNrm <-> A. x e. ~P U. J ( J |`t x ) e. Nrm ) )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 6 pweqd 
 |-  ( J e. ( TopOn ` X ) -> ~P X = ~P U. J )
8 7 raleqdv 
 |-  ( J e. ( TopOn ` X ) -> ( A. x e. ~P X ( J |`t x ) e. Nrm <-> A. x e. ~P U. J ( J |`t x ) e. Nrm ) )
9 5 8 bitr4d 
 |-  ( J e. ( TopOn ` X ) -> ( J e. CNrm <-> A. x e. ~P X ( J |`t x ) e. Nrm ) )