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 = U. J
paste.2
|- Y = U. K
paste.4
|- ( ph -> A e. ( Clsd ` J ) )
paste.5
|- ( ph -> B e. ( Clsd ` J ) )
paste.6
|- ( ph -> ( A u. B ) = X )
paste.7
|- ( ph -> F : X --> Y )
paste.8
|- ( ph -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
paste.9
|- ( ph -> ( F |` B ) e. ( ( J |`t B ) Cn K ) )
Assertion paste
|- ( ph -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 paste.1
 |-  X = U. J
2 paste.2
 |-  Y = U. K
3 paste.4
 |-  ( ph -> A e. ( Clsd ` J ) )
4 paste.5
 |-  ( ph -> B e. ( Clsd ` J ) )
5 paste.6
 |-  ( ph -> ( A u. B ) = X )
6 paste.7
 |-  ( ph -> F : X --> Y )
7 paste.8
 |-  ( ph -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
8 paste.9
 |-  ( ph -> ( F |` B ) e. ( ( J |`t B ) Cn K ) )
9 5 ineq2d
 |-  ( ph -> ( ( `' F " y ) i^i ( A u. B ) ) = ( ( `' F " y ) i^i X ) )
10 indi
 |-  ( ( `' F " y ) i^i ( A u. B ) ) = ( ( ( `' F " y ) i^i A ) u. ( ( `' F " y ) i^i B ) )
11 6 ffund
 |-  ( ph -> Fun F )
12 respreima
 |-  ( Fun F -> ( `' ( F |` A ) " y ) = ( ( `' F " y ) i^i A ) )
13 respreima
 |-  ( Fun F -> ( `' ( F |` B ) " y ) = ( ( `' F " y ) i^i B ) )
14 12 13 uneq12d
 |-  ( Fun F -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) = ( ( ( `' F " y ) i^i A ) u. ( ( `' F " y ) i^i B ) ) )
15 11 14 syl
 |-  ( ph -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) = ( ( ( `' F " y ) i^i A ) u. ( ( `' F " y ) i^i B ) ) )
16 10 15 eqtr4id
 |-  ( ph -> ( ( `' F " y ) i^i ( A u. B ) ) = ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) )
17 imassrn
 |-  ( `' F " y ) C_ ran `' F
18 dfdm4
 |-  dom F = ran `' F
19 fdm
 |-  ( F : X --> Y -> dom F = X )
20 18 19 eqtr3id
 |-  ( F : X --> Y -> ran `' F = X )
21 17 20 sseqtrid
 |-  ( F : X --> Y -> ( `' F " y ) C_ X )
22 6 21 syl
 |-  ( ph -> ( `' F " y ) C_ X )
23 df-ss
 |-  ( ( `' F " y ) C_ X <-> ( ( `' F " y ) i^i X ) = ( `' F " y ) )
24 22 23 sylib
 |-  ( ph -> ( ( `' F " y ) i^i X ) = ( `' F " y ) )
25 9 16 24 3eqtr3rd
 |-  ( ph -> ( `' F " y ) = ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) )
26 25 adantr
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' F " y ) = ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) )
27 cnclima
 |-  ( ( ( F |` A ) e. ( ( J |`t A ) Cn K ) /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` ( J |`t A ) ) )
28 7 27 sylan
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` ( J |`t A ) ) )
29 restcldr
 |-  ( ( A e. ( Clsd ` J ) /\ ( `' ( F |` A ) " y ) e. ( Clsd ` ( J |`t A ) ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` J ) )
30 3 28 29 syl2an2r
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` A ) " y ) e. ( Clsd ` J ) )
31 cnclima
 |-  ( ( ( F |` B ) e. ( ( J |`t B ) Cn K ) /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` ( J |`t B ) ) )
32 8 31 sylan
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` ( J |`t B ) ) )
33 restcldr
 |-  ( ( B e. ( Clsd ` J ) /\ ( `' ( F |` B ) " y ) e. ( Clsd ` ( J |`t B ) ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` J ) )
34 4 32 33 syl2an2r
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' ( F |` B ) " y ) e. ( Clsd ` J ) )
35 uncld
 |-  ( ( ( `' ( F |` A ) " y ) e. ( Clsd ` J ) /\ ( `' ( F |` B ) " y ) e. ( Clsd ` J ) ) -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) e. ( Clsd ` J ) )
36 30 34 35 syl2anc
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( ( `' ( F |` A ) " y ) u. ( `' ( F |` B ) " y ) ) e. ( Clsd ` J ) )
37 26 36 eqeltrd
 |-  ( ( ph /\ y e. ( Clsd ` K ) ) -> ( `' F " y ) e. ( Clsd ` J ) )
38 37 ralrimiva
 |-  ( ph -> A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) )
39 cldrcl
 |-  ( A e. ( Clsd ` J ) -> J e. Top )
40 3 39 syl
 |-  ( ph -> J e. Top )
41 cntop2
 |-  ( ( F |` A ) e. ( ( J |`t A ) Cn K ) -> K e. Top )
42 7 41 syl
 |-  ( ph -> K e. Top )
43 1 toptopon
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
44 2 toptopon
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
45 iscncl
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) )
46 43 44 45 syl2anb
 |-  ( ( J e. Top /\ K e. Top ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) )
47 40 42 46 syl2anc
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) )
48 6 38 47 mpbir2and
 |-  ( ph -> F e. ( J Cn K ) )