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 J Cn K J 𝑡 A Comp K 𝑡 F A Comp

Proof

Step Hyp Ref Expression
1 df-ima F A = ran F A
2 1 oveq2i K 𝑡 F A = K 𝑡 ran F A
3 simpr F J Cn K J 𝑡 A Comp J 𝑡 A Comp
4 simpl F J Cn K J 𝑡 A Comp F J Cn K
5 inss2 A J J
6 eqid J = J
7 6 cnrest F J Cn K A J J F A J J 𝑡 A J Cn K
8 4 5 7 sylancl F J Cn K J 𝑡 A Comp F A J J 𝑡 A J Cn K
9 resdmres F dom F A = F A
10 dmres dom F A = A dom F
11 eqid K = K
12 6 11 cnf F J Cn K F : J K
13 fdm F : J K dom F = J
14 4 12 13 3syl F J Cn K J 𝑡 A Comp dom F = J
15 14 ineq2d F J Cn K J 𝑡 A Comp A dom F = A J
16 10 15 syl5eq F J Cn K J 𝑡 A Comp dom F A = A J
17 16 reseq2d F J Cn K J 𝑡 A Comp F dom F A = F A J
18 9 17 eqtr3id F J Cn K J 𝑡 A Comp F A = F A J
19 cmptop J 𝑡 A Comp J 𝑡 A Top
20 19 adantl F J Cn K J 𝑡 A Comp J 𝑡 A Top
21 restrcl J 𝑡 A Top J V A V
22 6 restin J V A V J 𝑡 A = J 𝑡 A J
23 20 21 22 3syl F J Cn K J 𝑡 A Comp J 𝑡 A = J 𝑡 A J
24 23 oveq1d F J Cn K J 𝑡 A Comp J 𝑡 A Cn K = J 𝑡 A J Cn K
25 8 18 24 3eltr4d F J Cn K J 𝑡 A Comp F A J 𝑡 A Cn K
26 rncmp J 𝑡 A Comp F A J 𝑡 A Cn K K 𝑡 ran F A Comp
27 3 25 26 syl2anc F J Cn K J 𝑡 A Comp K 𝑡 ran F A Comp
28 2 27 eqeltrid F J Cn K J 𝑡 A Comp K 𝑡 F A Comp