Theorem cnrmi

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

	Ref	Expression
Assertion	cnrmi	$$⊢\left(J\in \mathrm{CNrm}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A\in \mathrm{Nrm}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup J=\bigcup J$$
2	1	restin	$$⊢\left(J\in \mathrm{CNrm}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(A\cap \bigcup J\right)$$
3		oveq2	$$⊢x=A\cap \bigcup J\to J{\upharpoonright }_{𝑡}x=J{\upharpoonright }_{𝑡}\left(A\cap \bigcup J\right)$$
4	3	eleq1d	$$⊢x=A\cap \bigcup J\to \left(J{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}\leftrightarrow J{\upharpoonright }_{𝑡}\left(A\cap \bigcup J\right)\in \mathrm{Nrm}\right)$$
5	1	iscnrm	$$⊢J\in \mathrm{CNrm}\leftrightarrow \left(J\in \mathrm{Top}\wedge \forall x\in 𝒫\bigcup JJ{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}\right)$$
6	5	simprbi	$$⊢J\in \mathrm{CNrm}\to \forall x\in 𝒫\bigcup JJ{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}$$
7	6	adantr	$$⊢\left(J\in \mathrm{CNrm}\wedge A\in V\right)\to \forall x\in 𝒫\bigcup JJ{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}$$
8		inss2	$$⊢A\cap \bigcup J\subseteq \bigcup J$$
9		inex1g	$$⊢A\in V\to A\cap \bigcup J\in \mathrm{V}$$
10		elpwg	$$⊢A\cap \bigcup J\in \mathrm{V}\to \left(A\cap \bigcup J\in 𝒫\bigcup J\leftrightarrow A\cap \bigcup J\subseteq \bigcup J\right)$$
11	9 10	syl	$$⊢A\in V\to \left(A\cap \bigcup J\in 𝒫\bigcup J\leftrightarrow A\cap \bigcup J\subseteq \bigcup J\right)$$
12	8 11	mpbiri	$$⊢A\in V\to A\cap \bigcup J\in 𝒫\bigcup J$$
13	12	adantl	$$⊢\left(J\in \mathrm{CNrm}\wedge A\in V\right)\to A\cap \bigcup J\in 𝒫\bigcup J$$
14	4 7 13	rspcdva	$$⊢\left(J\in \mathrm{CNrm}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}\left(A\cap \bigcup J\right)\in \mathrm{Nrm}$$
15	2 14	eqeltrd	$$⊢\left(J\in \mathrm{CNrm}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A\in \mathrm{Nrm}$$