Metamath Proof Explorer

Theorem 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 ⊢ φ → A ∈ Clsd ⁡ J
paste.5 ⊢ φ → B ∈ Clsd ⁡ J
paste.6 ⊢ φ → A ∪ B = X
paste.7 ⊢ φ → F : X ⟶ Y
paste.8 ⊢ φ → F ↾ A ∈ J ↾ 𝑡 A Cn K
paste.9 ⊢ φ → F ↾ B ∈ J ↾ 𝑡 B Cn K
Assertion paste ⊢ φ → F ∈ J Cn K

Proof

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