cnrmi

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

		Ref	Expression
	Assertion	cnrmi	$⊢ (J \in CNrm \land A \in V) \to J ↾_{𝑡} A \in Nrm$

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

Metamath Proof Explorer