Metamath Proof Explorer


Theorem rncmp

Description: The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion rncmp ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐾t ran 𝐹 ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Comp )
2 eqid 𝐽 = 𝐽
3 eqid 𝐾 = 𝐾
4 2 3 cnf ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝐽 𝐾 )
5 4 adantl ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝐽 𝐾 )
6 5 ffnd ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 Fn 𝐽 )
7 dffn4 ( 𝐹 Fn 𝐽𝐹 : 𝐽onto→ ran 𝐹 )
8 6 7 sylib ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝐽onto→ ran 𝐹 )
9 cntop2 ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
10 9 adantl ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ Top )
11 5 frnd ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ran 𝐹 𝐾 )
12 3 restuni ( ( 𝐾 ∈ Top ∧ ran 𝐹 𝐾 ) → ran 𝐹 = ( 𝐾t ran 𝐹 ) )
13 10 11 12 syl2anc ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ran 𝐹 = ( 𝐾t ran 𝐹 ) )
14 foeq3 ( ran 𝐹 = ( 𝐾t ran 𝐹 ) → ( 𝐹 : 𝐽onto→ ran 𝐹𝐹 : 𝐽onto ( 𝐾t ran 𝐹 ) ) )
15 13 14 syl ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝐽onto→ ran 𝐹𝐹 : 𝐽onto ( 𝐾t ran 𝐹 ) ) )
16 8 15 mpbid ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : 𝐽onto ( 𝐾t ran 𝐹 ) )
17 simpr ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
18 toptopon2 ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
19 10 18 sylib ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
20 ssidd ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ran 𝐹 ⊆ ran 𝐹 )
21 cnrest2 ( ( 𝐾 ∈ ( TopOn ‘ 𝐾 ) ∧ ran 𝐹 ⊆ ran 𝐹 ∧ ran 𝐹 𝐾 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾t ran 𝐹 ) ) ) )
22 19 20 11 21 syl3anc ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐹 ∈ ( 𝐽 Cn ( 𝐾t ran 𝐹 ) ) ) )
23 17 22 mpbid ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐾t ran 𝐹 ) ) )
24 eqid ( 𝐾t ran 𝐹 ) = ( 𝐾t ran 𝐹 )
25 24 cncmp ( ( 𝐽 ∈ Comp ∧ 𝐹 : 𝐽onto ( 𝐾t ran 𝐹 ) ∧ 𝐹 ∈ ( 𝐽 Cn ( 𝐾t ran 𝐹 ) ) ) → ( 𝐾t ran 𝐹 ) ∈ Comp )
26 1 16 23 25 syl3anc ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐾t ran 𝐹 ) ∈ Comp )