Metamath Proof Explorer

Theorem cnres2

Description: The restriction of a continuous function to a subset is continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypotheses cnres2.1 
|- X = U. J
cnres2.2 
|- Y = U. K
Assertion cnres2 
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t B ) ) )

Proof

Step Hyp Ref Expression
1 cnres2.1 
 |-  X = U. J
2 cnres2.2 
 |-  Y = U. K
3 simp3l 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> F e. ( J Cn K ) )
4 simp2l 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> A C_ X )
5 1 cnrest 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
6 3 4 5 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
7 simp1r 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> K e. Top )
8 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
9 7 8 sylib 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> K e. ( TopOn ` Y ) )
10 df-ima 
 |-  ( F " A ) = ran ( F |` A )
11 simp3r 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> A. x e. A ( F ` x ) e. B )
12 1 2 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> Y )
13 ffun 
 |-  ( F : X --> Y -> Fun F )
14 3 12 13 3syl 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> Fun F )
15 fdm 
 |-  ( F : X --> Y -> dom F = X )
16 3 12 15 3syl 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> dom F = X )
17 4 16 sseqtrrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> A C_ dom F )
18 funimass4 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
19 14 17 18 syl2anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
20 11 19 mpbird 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( F " A ) C_ B )
21 10 20 eqsstrrid 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ran ( F |` A ) C_ B )
22 simp2r 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> B C_ Y )
23 cnrest2 
 |-  ( ( K e. ( TopOn ` Y ) /\ ran ( F |` A ) C_ B /\ B C_ Y ) -> ( ( F |` A ) e. ( ( J |`t A ) Cn K ) <-> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t B ) ) ) )
24 9 21 22 23 syl3anc 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( ( F |` A ) e. ( ( J |`t A ) Cn K ) <-> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t B ) ) ) )
25 6 24 mpbid 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ ( A C_ X /\ B C_ Y ) /\ ( F e. ( J Cn K ) /\ A. x e. A ( F ` x ) e. B ) ) -> ( F |` A ) e. ( ( J |`t A ) Cn ( K |`t B ) ) )