paste

Description: Pasting lemma. If A and B are closed sets in X with A u. B = X , then any function whose restrictions to A and B are continuous is continuous on all of X . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypotheses	paste.1	$⊢ X = ⋃ J$
	paste.2	$⊢ Y = ⋃ K$
	paste.4	$⊢ φ \to A \in Clsd (J)$
	paste.5	$⊢ φ \to B \in Clsd (J)$
	paste.6	$⊢ φ \to A \cup B = X$
	paste.7	$⊢ φ \to F : X ⟶ Y$
	paste.8	$⊢ φ \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
	paste.9	$⊢ φ \to {F ↾}_{B} \in ((J ↾_{𝑡} B) Cn K)$
Assertion	paste	$⊢ φ \to F \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		paste.1	$⊢ X = ⋃ J$
2		paste.2	$⊢ Y = ⋃ K$
3		paste.4	$⊢ φ \to A \in Clsd (J)$
4		paste.5	$⊢ φ \to B \in Clsd (J)$
5		paste.6	$⊢ φ \to A \cup B = X$
6		paste.7	$⊢ φ \to F : X ⟶ Y$
7		paste.8	$⊢ φ \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
8		paste.9	$⊢ φ \to {F ↾}_{B} \in ((J ↾_{𝑡} B) Cn K)$
9	5	ineq2d	$⊢ φ \to F^{-1} [y] \cap (A \cup B) = F^{-1} [y] \cap X$
10		indi	$⊢ F^{-1} [y] \cap (A \cup B) = (F^{-1} [y] \cap A) \cup (F^{-1} [y] \cap B)$
11	6	ffund	$⊢ φ \to Fun F$
12		respreima	$⊢ Fun F \to {({F ↾}_{A})}^{-1} [y] = F^{-1} [y] \cap A$
13		respreima	$⊢ Fun F \to {({F ↾}_{B})}^{-1} [y] = F^{-1} [y] \cap B$
14	12 13	uneq12d	$⊢ Fun F \to {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y] = (F^{-1} [y] \cap A) \cup (F^{-1} [y] \cap B)$
15	11 14	syl	$⊢ φ \to {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y] = (F^{-1} [y] \cap A) \cup (F^{-1} [y] \cap B)$
16	10 15	eqtr4id	$⊢ φ \to F^{-1} [y] \cap (A \cup B) = {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y]$
17		imassrn	$⊢ F^{-1} [y] \subseteq ran F^{-1}$
18		dfdm4	$⊢ dom F = ran F^{-1}$
19		fdm	$⊢ F : X ⟶ Y \to dom F = X$
20	18 19	eqtr3id	$⊢ F : X ⟶ Y \to ran F^{-1} = X$
21	17 20	sseqtrid	$⊢ F : X ⟶ Y \to F^{-1} [y] \subseteq X$
22	6 21	syl	$⊢ φ \to F^{-1} [y] \subseteq X$
23		df-ss	$⊢ F^{-1} [y] \subseteq X \leftrightarrow F^{-1} [y] \cap X = F^{-1} [y]$
24	22 23	sylib	$⊢ φ \to F^{-1} [y] \cap X = F^{-1} [y]$
25	9 16 24	3eqtr3rd	$⊢ φ \to F^{-1} [y] = {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y]$
26	25	adantr	$⊢ (φ \land y \in Clsd (K)) \to F^{-1} [y] = {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y]$
27		cnclima	$⊢ ({F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \land y \in Clsd (K)) \to {({F ↾}_{A})}^{-1} [y] \in Clsd (J ↾_{𝑡} A)$
28	7 27	sylan	$⊢ (φ \land y \in Clsd (K)) \to {({F ↾}_{A})}^{-1} [y] \in Clsd (J ↾_{𝑡} A)$
29		restcldr	$⊢ (A \in Clsd (J) \land {({F ↾}_{A})}^{-1} [y] \in Clsd (J ↾_{𝑡} A)) \to {({F ↾}_{A})}^{-1} [y] \in Clsd (J)$
30	3 28 29	syl2an2r	$⊢ (φ \land y \in Clsd (K)) \to {({F ↾}_{A})}^{-1} [y] \in Clsd (J)$
31		cnclima	$⊢ ({F ↾}_{B} \in ((J ↾_{𝑡} B) Cn K) \land y \in Clsd (K)) \to {({F ↾}_{B})}^{-1} [y] \in Clsd (J ↾_{𝑡} B)$
32	8 31	sylan	$⊢ (φ \land y \in Clsd (K)) \to {({F ↾}_{B})}^{-1} [y] \in Clsd (J ↾_{𝑡} B)$
33		restcldr	$⊢ (B \in Clsd (J) \land {({F ↾}_{B})}^{-1} [y] \in Clsd (J ↾_{𝑡} B)) \to {({F ↾}_{B})}^{-1} [y] \in Clsd (J)$
34	4 32 33	syl2an2r	$⊢ (φ \land y \in Clsd (K)) \to {({F ↾}_{B})}^{-1} [y] \in Clsd (J)$
35		uncld	$⊢ ({({F ↾}_{A})}^{-1} [y] \in Clsd (J) \land {({F ↾}_{B})}^{-1} [y] \in Clsd (J)) \to {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y] \in Clsd (J)$
36	30 34 35	syl2anc	$⊢ (φ \land y \in Clsd (K)) \to {({F ↾}_{A})}^{-1} [y] \cup {({F ↾}_{B})}^{-1} [y] \in Clsd (J)$
37	26 36	eqeltrd	$⊢ (φ \land y \in Clsd (K)) \to F^{-1} [y] \in Clsd (J)$
38	37	ralrimiva	$⊢ φ \to \forall y \in Clsd (K) F^{-1} [y] \in Clsd (J)$
39		cldrcl	$⊢ A \in Clsd (J) \to J \in Top$
40	3 39	syl	$⊢ φ \to J \in Top$
41		cntop2	$⊢ {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K) \to K \in Top$
42	7 41	syl	$⊢ φ \to K \in Top$
43	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
44	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
45		iscncl	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in Clsd (K) F^{-1} [y] \in Clsd (J)))$
46	43 44 45	syl2anb	$⊢ (J \in Top \land K \in Top) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in Clsd (K) F^{-1} [y] \in Clsd (J)))$
47	40 42 46	syl2anc	$⊢ φ \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall y \in Clsd (K) F^{-1} [y] \in Clsd (J)))$
48	6 38 47	mpbir2and	$⊢ φ \to F \in (J Cn K)$

Metamath Proof Explorer

Theorem paste

Proof