This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnmpt1res

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

Ref Expression
Hypotheses cnmpt1res.2 
|- K = ( J |`t Y )
cnmpt1res.3 
|- ( ph -> J e. ( TopOn ` X ) )
cnmpt1res.5 
|- ( ph -> Y C_ X )
cnmpt1res.6 
|- ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )
Assertion cnmpt1res 
|- ( ph -> ( x e. Y |-> A ) e. ( K 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 cnmpt1res.6 
 |-  ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )
5 3 resmptd 
 |-  ( ph -> ( ( x e. X |-> A ) |` Y ) = ( x e. Y |-> A ) )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 2 6 syl 
 |-  ( ph -> X = U. J )
8 3 7 sseqtrd 
 |-  ( ph -> Y C_ U. J )
9 eqid 
 |-  U. J = U. J
10 9 cnrest 
 |-  ( ( ( x e. X |-> A ) e. ( J Cn L ) /\ Y C_ U. J ) -> ( ( x e. X |-> A ) |` Y ) e. ( ( J |`t Y ) Cn L ) )
11 4 8 10 syl2anc 
 |-  ( ph -> ( ( x e. X |-> A ) |` Y ) e. ( ( J |`t Y ) Cn L ) )
12 1 oveq1i 
 |-  ( K Cn L ) = ( ( J |`t Y ) Cn L )
13 11 12 eleqtrrdi 
 |-  ( ph -> ( ( x e. X |-> A ) |` Y ) e. ( K Cn L ) )
14 5 13 eqeltrrd 
 |-  ( ph -> ( x e. Y |-> A ) e. ( K Cn L ) )