cnrest

Description: Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Hypothesis	cnrest.1	$⊢ X = ⋃ J$
	Assertion	cnrest	$⊢ (F \in (J Cn K) \land A \subseteq X) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$

Proof

Step	Hyp	Ref	Expression
1		cnrest.1	$⊢ X = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ ⋃ K$
4	3	adantr	$⊢ (F \in (J Cn K) \land A \subseteq X) \to F : X ⟶ ⋃ K$
5		simpr	$⊢ (F \in (J Cn K) \land A \subseteq X) \to A \subseteq X$
6	4 5	fssresd	$⊢ (F \in (J Cn K) \land A \subseteq X) \to ({F ↾}_{A}) : A ⟶ ⋃ K$
7		cnvresima	$⊢ {({F ↾}_{A})}^{-1} [o] = F^{-1} [o] \cap A$
8		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
9	8	adantr	$⊢ (F \in (J Cn K) \land A \subseteq X) \to J \in Top$
10	9	adantr	$⊢ ((F \in (J Cn K) \land A \subseteq X) \land o \in K) \to J \in Top$
11	1	topopn	$⊢ J \in Top \to X \in J$
12		ssexg	$⊢ (A \subseteq X \land X \in J) \to A \in V$
13	12	ancoms	$⊢ (X \in J \land A \subseteq X) \to A \in V$
14	11 13	sylan	$⊢ (J \in Top \land A \subseteq X) \to A \in V$
15	8 14	sylan	$⊢ (F \in (J Cn K) \land A \subseteq X) \to A \in V$
16	15	adantr	$⊢ ((F \in (J Cn K) \land A \subseteq X) \land o \in K) \to A \in V$
17		cnima	$⊢ (F \in (J Cn K) \land o \in K) \to F^{-1} [o] \in J$
18	17	adantlr	$⊢ ((F \in (J Cn K) \land A \subseteq X) \land o \in K) \to F^{-1} [o] \in J$
19		elrestr	$⊢ (J \in Top \land A \in V \land F^{-1} [o] \in J) \to F^{-1} [o] \cap A \in (J ↾_{𝑡} A)$
20	10 16 18 19	syl3anc	$⊢ ((F \in (J Cn K) \land A \subseteq X) \land o \in K) \to F^{-1} [o] \cap A \in (J ↾_{𝑡} A)$
21	7 20	eqeltrid	$⊢ ((F \in (J Cn K) \land A \subseteq X) \land o \in K) \to {({F ↾}_{A})}^{-1} [o] \in (J ↾_{𝑡} A)$
22	21	ralrimiva	$⊢ (F \in (J Cn K) \land A \subseteq X) \to \forall o \in K {({F ↾}_{A})}^{-1} [o] \in (J ↾_{𝑡} A)$
23	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
24	8 23	sylib	$⊢ F \in (J Cn K) \to J \in TopOn (X)$
25		resttopon	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \in TopOn (A)$
26	24 25	sylan	$⊢ (F \in (J Cn K) \land A \subseteq X) \to J ↾_{𝑡} A \in TopOn (A)$
27		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
28	27	adantr	$⊢ (F \in (J Cn K) \land A \subseteq X) \to K \in Top$
29	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
30	28 29	sylib	$⊢ (F \in (J Cn K) \land A \subseteq X) \to K \in TopOn (⋃ K)$
31		iscn	$⊢ (J ↾_{𝑡} A \in TopOn (A) \land K \in TopOn (⋃ K)) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow (({F ↾}_{A}) : A ⟶ ⋃ K \land \forall o \in K {({F ↾}_{A})}^{-1} [o] \in (J ↾_{𝑡} A)))$
32	26 30 31	syl2anc	$⊢ (F \in (J Cn K) \land A \subseteq X) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow (({F ↾}_{A}) : A ⟶ ⋃ K \land \forall o \in K {({F ↾}_{A})}^{-1} [o] \in (J ↾_{𝑡} A)))$
33	6 22 32	mpbir2and	$⊢ (F \in (J Cn K) \land A \subseteq X) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$

Metamath Proof Explorer

Theorem cnrest

Proof