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 ) )