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 CNrm A V J 𝑡 A Nrm

Proof

Step Hyp Ref Expression
1 eqid J = J
2 1 restin J CNrm A V J 𝑡 A = J 𝑡 A J
3 oveq2 x = A J J 𝑡 x = J 𝑡 A J
4 3 eleq1d x = A J J 𝑡 x Nrm J 𝑡 A J Nrm
5 1 iscnrm J CNrm J Top x 𝒫 J J 𝑡 x Nrm
6 5 simprbi J CNrm x 𝒫 J J 𝑡 x Nrm
7 6 adantr J CNrm A V x 𝒫 J J 𝑡 x Nrm
8 inss2 A J J
9 inex1g A V A J V
10 elpwg A J V A J 𝒫 J A J J
11 9 10 syl A V A J 𝒫 J A J J
12 8 11 mpbiri A V A J 𝒫 J
13 12 adantl J CNrm A V A J 𝒫 J
14 4 7 13 rspcdva J CNrm A V J 𝑡 A J Nrm
15 2 14 eqeltrd J CNrm A V J 𝑡 A Nrm