This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnrmi

Description: A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion cnrmi 
|- ( ( J e. CNrm /\ A e. V ) -> ( J |`t A ) e. Nrm )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 restin 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( J |`t A ) = ( J |`t ( A i^i U. J ) ) )
3 oveq2 
 |-  ( x = ( A i^i U. J ) -> ( J |`t x ) = ( J |`t ( A i^i U. J ) ) )
4 3 eleq1d 
 |-  ( x = ( A i^i U. J ) -> ( ( J |`t x ) e. Nrm <-> ( J |`t ( A i^i U. J ) ) e. Nrm ) )
5 1 iscnrm 
 |-  ( J e. CNrm <-> ( J e. Top /\ A. x e. ~P U. J ( J |`t x ) e. Nrm ) )
6 5 simprbi 
 |-  ( J e. CNrm -> A. x e. ~P U. J ( J |`t x ) e. Nrm )
7 6 adantr 
 |-  ( ( J e. CNrm /\ A e. V ) -> A. x e. ~P U. J ( J |`t x ) e. Nrm )
8 inss2 
 |-  ( A i^i U. J ) C_ U. J
9 inex1g 
 |-  ( A e. V -> ( A i^i U. J ) e. _V )
10 elpwg 
 |-  ( ( A i^i U. J ) e. _V -> ( ( A i^i U. J ) e. ~P U. J <-> ( A i^i U. J ) C_ U. J ) )
11 9 10 syl 
 |-  ( A e. V -> ( ( A i^i U. J ) e. ~P U. J <-> ( A i^i U. J ) C_ U. J ) )
12 8 11 mpbiri 
 |-  ( A e. V -> ( A i^i U. J ) e. ~P U. J )
13 12 adantl 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( A i^i U. J ) e. ~P U. J )
14 4 7 13 rspcdva 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( J |`t ( A i^i U. J ) ) e. Nrm )
15 2 14 eqeltrd 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( J |`t A ) e. Nrm )