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 ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐾t ( 𝐹𝐴 ) ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 df-ima ( 𝐹𝐴 ) = ran ( 𝐹𝐴 )
2 1 oveq2i ( 𝐾t ( 𝐹𝐴 ) ) = ( 𝐾t ran ( 𝐹𝐴 ) )
3 simpr ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐽t 𝐴 ) ∈ Comp )
4 simpl ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5 inss2 ( 𝐴 𝐽 ) ⊆ 𝐽
6 eqid 𝐽 = 𝐽
7 6 cnrest ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐴 𝐽 ) ⊆ 𝐽 ) → ( 𝐹 ↾ ( 𝐴 𝐽 ) ) ∈ ( ( 𝐽t ( 𝐴 𝐽 ) ) Cn 𝐾 ) )
8 4 5 7 sylancl ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐹 ↾ ( 𝐴 𝐽 ) ) ∈ ( ( 𝐽t ( 𝐴 𝐽 ) ) Cn 𝐾 ) )
9 resdmres ( 𝐹 ↾ dom ( 𝐹𝐴 ) ) = ( 𝐹𝐴 )
10 dmres dom ( 𝐹𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
11 eqid 𝐾 = 𝐾
12 6 11 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝐽 𝐾 )
13 fdm ( 𝐹 : 𝐽 𝐾 → dom 𝐹 = 𝐽 )
14 4 12 13 3syl ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → dom 𝐹 = 𝐽 )
15 14 ineq2d ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐴 ∩ dom 𝐹 ) = ( 𝐴 𝐽 ) )
16 10 15 syl5eq ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → dom ( 𝐹𝐴 ) = ( 𝐴 𝐽 ) )
17 16 reseq2d ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐹 ↾ dom ( 𝐹𝐴 ) ) = ( 𝐹 ↾ ( 𝐴 𝐽 ) ) )
18 9 17 eqtr3id ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐹𝐴 ) = ( 𝐹 ↾ ( 𝐴 𝐽 ) ) )
19 cmptop ( ( 𝐽t 𝐴 ) ∈ Comp → ( 𝐽t 𝐴 ) ∈ Top )
20 19 adantl ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐽t 𝐴 ) ∈ Top )
21 restrcl ( ( 𝐽t 𝐴 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) )
22 6 restin ( ( 𝐽 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐽t 𝐴 ) = ( 𝐽t ( 𝐴 𝐽 ) ) )
23 20 21 22 3syl ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐽t 𝐴 ) = ( 𝐽t ( 𝐴 𝐽 ) ) )
24 23 oveq1d ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( ( 𝐽t 𝐴 ) Cn 𝐾 ) = ( ( 𝐽t ( 𝐴 𝐽 ) ) Cn 𝐾 ) )
25 8 18 24 3eltr4d ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐾 ) )
26 rncmp ( ( ( 𝐽t 𝐴 ) ∈ Comp ∧ ( 𝐹𝐴 ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐾 ) ) → ( 𝐾t ran ( 𝐹𝐴 ) ) ∈ Comp )
27 3 25 26 syl2anc ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐾t ran ( 𝐹𝐴 ) ) ∈ Comp )
28 2 27 eqeltrid ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝐽t 𝐴 ) ∈ Comp ) → ( 𝐾t ( 𝐹𝐴 ) ) ∈ Comp )