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 ⊢ 𝑋 = ∪ 𝐽
paste.2 ⊢ 𝑌 = ∪ 𝐾
paste.4 ⊢ ( 𝜑 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
paste.5 ⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
paste.6 ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = 𝑋 )
paste.7 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
paste.8 ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
paste.9 ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ ( ( 𝐽 ↾t 𝐵 ) Cn 𝐾 ) )
Assertion paste ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 paste.1 ⊢ 𝑋 = ∪ 𝐽
2 paste.2 ⊢ 𝑌 = ∪ 𝐾
3 paste.4 ⊢ ( 𝜑 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
4 paste.5 ⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
5 paste.6 ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = 𝑋 )
6 paste.7 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
7 paste.8 ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) )
8 paste.9 ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ ( ( 𝐽 ↾t 𝐵 ) Cn 𝐾 ) )
9 5 ineq2d ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝑋 ) )
10 indi ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐴 ) ∪ ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐵 ) )
11 6 ffund ⊢ ( 𝜑 → Fun 𝐹 )
12 respreima ⊢ ( Fun 𝐹 → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) = ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐴 ) )
13 respreima ⊢ ( Fun 𝐹 → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) = ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐵 ) )
14 12 13 uneq12d ⊢ ( Fun 𝐹 → ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) = ( ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐴 ) ∪ ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐵 ) ) )
15 11 14 syl ⊢ ( 𝜑 → ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) = ( ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐴 ) ∪ ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝐵 ) ) )
16 10 15 eqtr4id ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( 𝐴 ∪ 𝐵 ) ) = ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) )
17 imassrn ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ ran ◡ 𝐹
18 dfdm4 ⊢ dom 𝐹 = ran ◡ 𝐹
19 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
20 18 19 eqtr3id ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ran ◡ 𝐹 = 𝑋 )
21 17 20 sseqtrid ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
22 6 21 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 )
23 dfss2 ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝑋 ↔ ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑦 ) )
24 22 23 sylib ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑦 ) ∩ 𝑋 ) = ( ◡ 𝐹 “ 𝑦 ) )
25 9 16 24 3eqtr3rd ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑦 ) = ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑦 ) = ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) )
27 cnclima ⊢ ( ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) )
28 7 27 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) )
29 restcldr ⊢ ( ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
30 3 28 29 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
31 cnclima ⊢ ( ( ( 𝐹 ↾ 𝐵 ) ∈ ( ( 𝐽 ↾t 𝐵 ) Cn 𝐾 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐵 ) ) )
32 8 31 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐵 ) ) )
33 restcldr ⊢ ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐵 ) ) ) → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
34 4 32 33 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
35 uncld ⊢ ( ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
36 30 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑦 ) ∪ ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑦 ) ) ∈ ( Clsd ‘ 𝐽 ) )
37 26 36 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
38 37 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
39 cldrcl ⊢ ( 𝐴 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
40 3 39 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
41 cntop2 ⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) → 𝐾 ∈ Top )
42 7 41 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
43 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
44 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
45 iscncl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
46 43 44 45 syl2anb ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
47 40 42 46 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( Clsd ‘ 𝐾 ) ( ◡ 𝐹 “ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
48 6 38 47 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )