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 )