restcnrm

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

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

Proof

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		simpll	$⊢ ((J \in CNrm \land A \in V) \land x \in 𝒫 (A \cap ⋃ J)) \to J \in CNrm$
4		elpwi	$⊢ x \in 𝒫 (A \cap ⋃ J) \to x \subseteq A \cap ⋃ J$
5	4	adantl	$⊢ ((J \in CNrm \land A \in V) \land x \in 𝒫 (A \cap ⋃ J)) \to x \subseteq A \cap ⋃ J$
6		inex1g	$⊢ A \in V \to A \cap ⋃ J \in V$
7	6	ad2antlr	$⊢ ((J \in CNrm \land A \in V) \land x \in 𝒫 (A \cap ⋃ J)) \to A \cap ⋃ J \in V$
8		restabs	$⊢ (J \in CNrm \land x \subseteq A \cap ⋃ J \land A \cap ⋃ J \in V) \to (J ↾_{𝑡} (A \cap ⋃ J)) ↾_{𝑡} x = J ↾_{𝑡} x$
9	3 5 7 8	syl3anc	$⊢ ((J \in CNrm \land A \in V) \land x \in 𝒫 (A \cap ⋃ J)) \to (J ↾_{𝑡} (A \cap ⋃ J)) ↾_{𝑡} x = J ↾_{𝑡} x$
10		cnrmi	$⊢ (J \in CNrm \land x \in 𝒫 (A \cap ⋃ J)) \to J ↾_{𝑡} x \in Nrm$
11	10	adantlr	$⊢ ((J \in CNrm \land A \in V) \land x \in 𝒫 (A \cap ⋃ J)) \to J ↾_{𝑡} x \in Nrm$
12	9 11	eqeltrd	$⊢ ((J \in CNrm \land A \in V) \land x \in 𝒫 (A \cap ⋃ J)) \to (J ↾_{𝑡} (A \cap ⋃ J)) ↾_{𝑡} x \in Nrm$
13	12	ralrimiva	$⊢ (J \in CNrm \land A \in V) \to \forall x \in 𝒫 (A \cap ⋃ J) (J ↾_{𝑡} (A \cap ⋃ J)) ↾_{𝑡} x \in Nrm$
14		cnrmtop	$⊢ J \in CNrm \to J \in Top$
15	14	adantr	$⊢ (J \in CNrm \land A \in V) \to J \in Top$
16		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
17	15 16	sylib	$⊢ (J \in CNrm \land A \in V) \to J \in TopOn (⋃ J)$
18		inss2	$⊢ A \cap ⋃ J \subseteq ⋃ J$
19		resttopon	$⊢ (J \in TopOn (⋃ J) \land A \cap ⋃ J \subseteq ⋃ J) \to J ↾_{𝑡} (A \cap ⋃ J) \in TopOn (A \cap ⋃ J)$
20	17 18 19	sylancl	$⊢ (J \in CNrm \land A \in V) \to J ↾_{𝑡} (A \cap ⋃ J) \in TopOn (A \cap ⋃ J)$
21		iscnrm2	$⊢ J ↾_{𝑡} (A \cap ⋃ J) \in TopOn (A \cap ⋃ J) \to (J ↾_{𝑡} (A \cap ⋃ J) \in CNrm \leftrightarrow \forall x \in 𝒫 (A \cap ⋃ J) (J ↾_{𝑡} (A \cap ⋃ J)) ↾_{𝑡} x \in Nrm)$
22	20 21	syl	$⊢ (J \in CNrm \land A \in V) \to (J ↾_{𝑡} (A \cap ⋃ J) \in CNrm \leftrightarrow \forall x \in 𝒫 (A \cap ⋃ J) (J ↾_{𝑡} (A \cap ⋃ J)) ↾_{𝑡} x \in Nrm)$
23	13 22	mpbird	$⊢ (J \in CNrm \land A \in V) \to J ↾_{𝑡} (A \cap ⋃ J) \in CNrm$
24	2 23	eqeltrd	$⊢ (J \in CNrm \land A \in V) \to J ↾_{𝑡} A \in CNrm$

Metamath Proof Explorer

Theorem restcnrm

Proof