Metamath Proof Explorer

Theorem restcnrm

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

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

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 simpll 
 |-  ( ( ( J e. CNrm /\ A e. V ) /\ x e. ~P ( A i^i U. J ) ) -> J e. CNrm )
4 elpwi 
 |-  ( x e. ~P ( A i^i U. J ) -> x C_ ( A i^i U. J ) )
5 4 adantl 
 |-  ( ( ( J e. CNrm /\ A e. V ) /\ x e. ~P ( A i^i U. J ) ) -> x C_ ( A i^i U. J ) )
6 inex1g 
 |-  ( A e. V -> ( A i^i U. J ) e. _V )
7 6 ad2antlr 
 |-  ( ( ( J e. CNrm /\ A e. V ) /\ x e. ~P ( A i^i U. J ) ) -> ( A i^i U. J ) e. _V )
8 restabs 
 |-  ( ( J e. CNrm /\ x C_ ( A i^i U. J ) /\ ( A i^i U. J ) e. _V ) -> ( ( J |`t ( A i^i U. J ) ) |`t x ) = ( J |`t x ) )
9 3 5 7 8 syl3anc 
 |-  ( ( ( J e. CNrm /\ A e. V ) /\ x e. ~P ( A i^i U. J ) ) -> ( ( J |`t ( A i^i U. J ) ) |`t x ) = ( J |`t x ) )
10 cnrmi 
 |-  ( ( J e. CNrm /\ x e. ~P ( A i^i U. J ) ) -> ( J |`t x ) e. Nrm )
11 10 adantlr 
 |-  ( ( ( J e. CNrm /\ A e. V ) /\ x e. ~P ( A i^i U. J ) ) -> ( J |`t x ) e. Nrm )
12 9 11 eqeltrd 
 |-  ( ( ( J e. CNrm /\ A e. V ) /\ x e. ~P ( A i^i U. J ) ) -> ( ( J |`t ( A i^i U. J ) ) |`t x ) e. Nrm )
13 12 ralrimiva 
 |-  ( ( J e. CNrm /\ A e. V ) -> A. x e. ~P ( A i^i U. J ) ( ( J |`t ( A i^i U. J ) ) |`t x ) e. Nrm )
14 cnrmtop 
 |-  ( J e. CNrm -> J e. Top )
15 14 adantr 
 |-  ( ( J e. CNrm /\ A e. V ) -> J e. Top )
16 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
17 15 16 sylib 
 |-  ( ( J e. CNrm /\ A e. V ) -> J e. ( TopOn ` U. J ) )
18 inss2 
 |-  ( A i^i U. J ) C_ U. J
19 resttopon 
 |-  ( ( J e. ( TopOn ` U. J ) /\ ( A i^i U. J ) C_ U. J ) -> ( J |`t ( A i^i U. J ) ) e. ( TopOn ` ( A i^i U. J ) ) )
20 17 18 19 sylancl 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( J |`t ( A i^i U. J ) ) e. ( TopOn ` ( A i^i U. J ) ) )
21 iscnrm2 
 |-  ( ( J |`t ( A i^i U. J ) ) e. ( TopOn ` ( A i^i U. J ) ) -> ( ( J |`t ( A i^i U. J ) ) e. CNrm <-> A. x e. ~P ( A i^i U. J ) ( ( J |`t ( A i^i U. J ) ) |`t x ) e. Nrm ) )
22 20 21 syl 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( ( J |`t ( A i^i U. J ) ) e. CNrm <-> A. x e. ~P ( A i^i U. J ) ( ( J |`t ( A i^i U. J ) ) |`t x ) e. Nrm ) )
23 13 22 mpbird 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( J |`t ( A i^i U. J ) ) e. CNrm )
24 2 23 eqeltrd 
 |-  ( ( J e. CNrm /\ A e. V ) -> ( J |`t A ) e. CNrm )