cnrest2r

Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 7-Jun-2014)

		Ref	Expression
	Assertion	cnrest2r	$⊢ K \in Top \to J Cn (K ↾_{𝑡} B) \subseteq J Cn K$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to f \in (J Cn (K ↾_{𝑡} B))$
2		cntop2	$⊢ f \in (J Cn (K ↾_{𝑡} B)) \to K ↾_{𝑡} B \in Top$
3	2	adantl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K ↾_{𝑡} B \in Top$
4		restrcl	$⊢ K ↾_{𝑡} B \in Top \to (K \in V \land B \in V)$
5		eqid	$⊢ ⋃ K = ⋃ K$
6	5	restin	$⊢ (K \in V \land B \in V) \to K ↾_{𝑡} B = K ↾_{𝑡} (B \cap ⋃ K)$
7	3 4 6	3syl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K ↾_{𝑡} B = K ↾_{𝑡} (B \cap ⋃ K)$
8	7	oveq2d	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to J Cn (K ↾_{𝑡} B) = J Cn (K ↾_{𝑡} (B \cap ⋃ K))$
9	1 8	eleqtrd	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to f \in (J Cn (K ↾_{𝑡} (B \cap ⋃ K)))$
10		simpl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K \in Top$
11		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
12	10 11	sylib	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K \in TopOn (⋃ K)$
13		cntop1	$⊢ f \in (J Cn (K ↾_{𝑡} B)) \to J \in Top$
14	13	adantl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to J \in Top$
15		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
16	14 15	sylib	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to J \in TopOn (⋃ J)$
17		inss2	$⊢ B \cap ⋃ K \subseteq ⋃ K$
18		resttopon	$⊢ (K \in TopOn (⋃ K) \land B \cap ⋃ K \subseteq ⋃ K) \to K ↾_{𝑡} (B \cap ⋃ K) \in TopOn (B \cap ⋃ K)$
19	12 17 18	sylancl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K ↾_{𝑡} (B \cap ⋃ K) \in TopOn (B \cap ⋃ K)$
20		cnf2	$⊢ (J \in TopOn (⋃ J) \land K ↾_{𝑡} (B \cap ⋃ K) \in TopOn (B \cap ⋃ K) \land f \in (J Cn (K ↾_{𝑡} (B \cap ⋃ K)))) \to f : ⋃ J ⟶ B \cap ⋃ K$
21	16 19 9 20	syl3anc	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to f : ⋃ J ⟶ B \cap ⋃ K$
22	21	frnd	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to ran f \subseteq B \cap ⋃ K$
23	17	a1i	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to B \cap ⋃ K \subseteq ⋃ K$
24		cnrest2	$⊢ (K \in TopOn (⋃ K) \land ran f \subseteq B \cap ⋃ K \land B \cap ⋃ K \subseteq ⋃ K) \to (f \in (J Cn K) \leftrightarrow f \in (J Cn (K ↾_{𝑡} (B \cap ⋃ K))))$
25	12 22 23 24	syl3anc	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to (f \in (J Cn K) \leftrightarrow f \in (J Cn (K ↾_{𝑡} (B \cap ⋃ K))))$
26	9 25	mpbird	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to f \in (J Cn K)$
27	26	ex	$⊢ K \in Top \to (f \in (J Cn (K ↾_{𝑡} B)) \to f \in (J Cn K))$
28	27	ssrdv	$⊢ K \in Top \to J Cn (K ↾_{𝑡} B) \subseteq J Cn K$

Metamath Proof Explorer

Theorem cnrest2r

Proof