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		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
11	10	birani	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K \in TopOn (⋃ K)$
12		cntop1	$⊢ f \in (J Cn (K ↾_{𝑡} B)) \to J \in Top$
13	12	adantl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to J \in Top$
14		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
15	13 14	sylib	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to J \in TopOn (⋃ J)$
16		inss2	$⊢ B \cap ⋃ K \subseteq ⋃ K$
17		resttopon	$⊢ (K \in TopOn (⋃ K) \land B \cap ⋃ K \subseteq ⋃ K) \to K ↾_{𝑡} (B \cap ⋃ K) \in TopOn (B \cap ⋃ K)$
18	11 16 17	sylancl	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to K ↾_{𝑡} (B \cap ⋃ K) \in TopOn (B \cap ⋃ K)$
19		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$
20	15 18 9 19	syl3anc	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to f : ⋃ J ⟶ B \cap ⋃ K$
21	20	frnd	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to ran f \subseteq B \cap ⋃ K$
22	16	a1i	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to B \cap ⋃ K \subseteq ⋃ K$
23		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))))$
24	11 21 22 23	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))))$
25	9 24	mpbird	$⊢ (K \in Top \land f \in (J Cn (K ↾_{𝑡} B))) \to f \in (J Cn K)$
26	25	ex	$⊢ K \in Top \to (f \in (J Cn (K ↾_{𝑡} B)) \to f \in (J Cn K))$
27	26	ssrdv	$⊢ K \in Top \to J Cn (K ↾_{𝑡} B) \subseteq J Cn K$

Metamath Proof Explorer

Theorem cnrest2r

Proof