Metamath Proof Explorer

Theorem cnrest

Description: Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypothesis cnrest.1 
|- X = U. J
Assertion cnrest 
|- ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )

Proof

Step Hyp Ref Expression
1 cnrest.1 
 |-  X = U. J
2 eqid 
 |-  U. K = U. K
3 1 2 cnf 
 |-  ( F e. ( J Cn K ) -> F : X --> U. K )
4 3 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> F : X --> U. K )
5 simpr 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> A C_ X )
6 4 5 fssresd 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) : A --> U. K )
7 cnvresima 
 |-  ( `' ( F |` A ) " o ) = ( ( `' F " o ) i^i A )
8 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
9 8 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> J e. Top )
10 9 adantr 
 |-  ( ( ( F e. ( J Cn K ) /\ A C_ X ) /\ o e. K ) -> J e. Top )
11 1 topopn 
 |-  ( J e. Top -> X e. J )
12 ssexg 
 |-  ( ( A C_ X /\ X e. J ) -> A e. _V )
13 12 ancoms 
 |-  ( ( X e. J /\ A C_ X ) -> A e. _V )
14 11 13 sylan 
 |-  ( ( J e. Top /\ A C_ X ) -> A e. _V )
15 8 14 sylan 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> A e. _V )
16 15 adantr 
 |-  ( ( ( F e. ( J Cn K ) /\ A C_ X ) /\ o e. K ) -> A e. _V )
17 cnima 
 |-  ( ( F e. ( J Cn K ) /\ o e. K ) -> ( `' F " o ) e. J )
18 17 adantlr 
 |-  ( ( ( F e. ( J Cn K ) /\ A C_ X ) /\ o e. K ) -> ( `' F " o ) e. J )
19 elrestr 
 |-  ( ( J e. Top /\ A e. _V /\ ( `' F " o ) e. J ) -> ( ( `' F " o ) i^i A ) e. ( J |`t A ) )
20 10 16 18 19 syl3anc 
 |-  ( ( ( F e. ( J Cn K ) /\ A C_ X ) /\ o e. K ) -> ( ( `' F " o ) i^i A ) e. ( J |`t A ) )
21 7 20 eqeltrid 
 |-  ( ( ( F e. ( J Cn K ) /\ A C_ X ) /\ o e. K ) -> ( `' ( F |` A ) " o ) e. ( J |`t A ) )
22 21 ralrimiva 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> A. o e. K ( `' ( F |` A ) " o ) e. ( J |`t A ) )
23 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
24 8 23 sylib 
 |-  ( F e. ( J Cn K ) -> J e. ( TopOn ` X ) )
25 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
26 24 25 sylan 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
27 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
28 27 adantr 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> K e. Top )
29 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
30 28 29 sylib 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> K e. ( TopOn ` U. K ) )
31 iscn 
 |-  ( ( ( J |`t A ) e. ( TopOn ` A ) /\ K e. ( TopOn ` U. K ) ) -> ( ( F |` A ) e. ( ( J |`t A ) Cn K ) <-> ( ( F |` A ) : A --> U. K /\ A. o e. K ( `' ( F |` A ) " o ) e. ( J |`t A ) ) ) )
32 26 30 31 syl2anc 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( ( F |` A ) e. ( ( J |`t A ) Cn K ) <-> ( ( F |` A ) : A --> U. K /\ A. o e. K ( `' ( F |` A ) " o ) e. ( J |`t A ) ) ) )
33 6 22 32 mpbir2and 
 |-  ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )