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 )