Metamath Proof Explorer

Theorem imacmp

Description: The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 18-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion imacmp 
|- ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( K |`t ( F " A ) ) e. Comp )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " A ) = ran ( F |` A )
2 1 oveq2i 
 |-  ( K |`t ( F " A ) ) = ( K |`t ran ( F |` A ) )
3 simpr 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( J |`t A ) e. Comp )
4 simpl 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> F e. ( J Cn K ) )
5 inss2 
 |-  ( A i^i U. J ) C_ U. J
6 eqid 
 |-  U. J = U. J
7 6 cnrest 
 |-  ( ( F e. ( J Cn K ) /\ ( A i^i U. J ) C_ U. J ) -> ( F |` ( A i^i U. J ) ) e. ( ( J |`t ( A i^i U. J ) ) Cn K ) )
8 4 5 7 sylancl 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( F |` ( A i^i U. J ) ) e. ( ( J |`t ( A i^i U. J ) ) Cn K ) )
9 resdmres 
 |-  ( F |` dom ( F |` A ) ) = ( F |` A )
10 dmres 
 |-  dom ( F |` A ) = ( A i^i dom F )
11 eqid 
 |-  U. K = U. K
12 6 11 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
13 fdm 
 |-  ( F : U. J --> U. K -> dom F = U. J )
14 4 12 13 3syl 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> dom F = U. J )
15 14 ineq2d 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( A i^i dom F ) = ( A i^i U. J ) )
16 10 15 eqtrid 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> dom ( F |` A ) = ( A i^i U. J ) )
17 16 reseq2d 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( F |` dom ( F |` A ) ) = ( F |` ( A i^i U. J ) ) )
18 9 17 eqtr3id 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( F |` A ) = ( F |` ( A i^i U. J ) ) )
19 cmptop 
 |-  ( ( J |`t A ) e. Comp -> ( J |`t A ) e. Top )
20 19 adantl 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( J |`t A ) e. Top )
21 restrcl 
 |-  ( ( J |`t A ) e. Top -> ( J e. _V /\ A e. _V ) )
22 6 restin 
 |-  ( ( J e. _V /\ A e. _V ) -> ( J |`t A ) = ( J |`t ( A i^i U. J ) ) )
23 20 21 22 3syl 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( J |`t A ) = ( J |`t ( A i^i U. J ) ) )
24 23 oveq1d 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( ( J |`t A ) Cn K ) = ( ( J |`t ( A i^i U. J ) ) Cn K ) )
25 8 18 24 3eltr4d 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( F |` A ) e. ( ( J |`t A ) Cn K ) )
26 rncmp 
 |-  ( ( ( J |`t A ) e. Comp /\ ( F |` A ) e. ( ( J |`t A ) Cn K ) ) -> ( K |`t ran ( F |` A ) ) e. Comp )
27 3 25 26 syl2anc 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( K |`t ran ( F |` A ) ) e. Comp )
28 2 27 eqeltrid 
 |-  ( ( F e. ( J Cn K ) /\ ( J |`t A ) e. Comp ) -> ( K |`t ( F " A ) ) e. Comp )