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 eqtrid ⊢ ( ( 𝐹 ∈ ( 𝐽 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 )