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 syl5eq
 |-  ( ( 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 )