Metamath Proof Explorer

Theorem cnmpt2res

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014)

Ref Expression
Hypotheses cnmpt1res.2 
|- K = ( J |`t Y )
cnmpt1res.3 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt1res.5 
|- ( ph -> Y C_ X )
cnmpt2res.7 
|- N = ( M |`t W )
cnmpt2res.8 
|- ( ph -> M e. ( TopOn ` Z ) )
cnmpt2res.9 
|- ( ph -> W C_ Z )
cnmpt2res.10 
|- ( ph -> ( x e. X , y e. Z |-> A ) e. ( ( J tX M ) Cn L ) )
Assertion cnmpt2res 
|- ( ph -> ( x e. Y , y e. W |-> A ) e. ( ( K tX N ) Cn L ) )

Proof

Step Hyp Ref Expression
1 cnmpt1res.2 
 |-  K = ( J |`t Y )
2 cnmpt1res.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 cnmpt1res.5 
 |-  ( ph -> Y C_ X )
4 cnmpt2res.7 
 |-  N = ( M |`t W )
5 cnmpt2res.8 
 |-  ( ph -> M e. ( TopOn ` Z ) )
6 cnmpt2res.9 
 |-  ( ph -> W C_ Z )
7 cnmpt2res.10 
 |-  ( ph -> ( x e. X , y e. Z |-> A ) e. ( ( J tX M ) Cn L ) )
8 xpss12 
 |-  ( ( Y C_ X /\ W C_ Z ) -> ( Y X. W ) C_ ( X X. Z ) )
9 3 6 8 syl2anc 
 |-  ( ph -> ( Y X. W ) C_ ( X X. Z ) )
10 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ M e. ( TopOn ` Z ) ) -> ( J tX M ) e. ( TopOn ` ( X X. Z ) ) )
11 2 5 10 syl2anc 
 |-  ( ph -> ( J tX M ) e. ( TopOn ` ( X X. Z ) ) )
12 toponuni 
 |-  ( ( J tX M ) e. ( TopOn ` ( X X. Z ) ) -> ( X X. Z ) = U. ( J tX M ) )
13 11 12 syl 
 |-  ( ph -> ( X X. Z ) = U. ( J tX M ) )
14 9 13 sseqtrd 
 |-  ( ph -> ( Y X. W ) C_ U. ( J tX M ) )
15 eqid 
 |-  U. ( J tX M ) = U. ( J tX M )
16 15 cnrest 
 |-  ( ( ( x e. X , y e. Z |-> A ) e. ( ( J tX M ) Cn L ) /\ ( Y X. W ) C_ U. ( J tX M ) ) -> ( ( x e. X , y e. Z |-> A ) |` ( Y X. W ) ) e. ( ( ( J tX M ) |`t ( Y X. W ) ) Cn L ) )
17 7 14 16 syl2anc 
 |-  ( ph -> ( ( x e. X , y e. Z |-> A ) |` ( Y X. W ) ) e. ( ( ( J tX M ) |`t ( Y X. W ) ) Cn L ) )
18 resmpo 
 |-  ( ( Y C_ X /\ W C_ Z ) -> ( ( x e. X , y e. Z |-> A ) |` ( Y X. W ) ) = ( x e. Y , y e. W |-> A ) )
19 3 6 18 syl2anc 
 |-  ( ph -> ( ( x e. X , y e. Z |-> A ) |` ( Y X. W ) ) = ( x e. Y , y e. W |-> A ) )
20 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
21 2 20 syl 
 |-  ( ph -> J e. Top )
22 topontop 
 |-  ( M e. ( TopOn ` Z ) -> M e. Top )
23 5 22 syl 
 |-  ( ph -> M e. Top )
24 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
25 2 24 syl 
 |-  ( ph -> X e. J )
26 25 3 ssexd 
 |-  ( ph -> Y e. _V )
27 toponmax 
 |-  ( M e. ( TopOn ` Z ) -> Z e. M )
28 5 27 syl 
 |-  ( ph -> Z e. M )
29 28 6 ssexd 
 |-  ( ph -> W e. _V )
30 txrest 
 |-  ( ( ( J e. Top /\ M e. Top ) /\ ( Y e. _V /\ W e. _V ) ) -> ( ( J tX M ) |`t ( Y X. W ) ) = ( ( J |`t Y ) tX ( M |`t W ) ) )
31 21 23 26 29 30 syl22anc 
 |-  ( ph -> ( ( J tX M ) |`t ( Y X. W ) ) = ( ( J |`t Y ) tX ( M |`t W ) ) )
32 1 4 oveq12i 
 |-  ( K tX N ) = ( ( J |`t Y ) tX ( M |`t W ) )
33 31 32 eqtr4di 
 |-  ( ph -> ( ( J tX M ) |`t ( Y X. W ) ) = ( K tX N ) )
34 33 oveq1d 
 |-  ( ph -> ( ( ( J tX M ) |`t ( Y X. W ) ) Cn L ) = ( ( K tX N ) Cn L ) )
35 17 19 34 3eltr3d 
 |-  ( ph -> ( x e. Y , y e. W |-> A ) e. ( ( K tX N ) Cn L ) )