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	$⊢ (J \in Comp \land F \in (J Cn K)) \to K ↾_{𝑡} ran F \in Comp$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (J \in Comp \land F \in (J Cn K)) \to J \in Comp$
2		eqid	$⊢ ⋃ J = ⋃ J$
3		eqid	$⊢ ⋃ K = ⋃ K$
4	2 3	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
5	4	adantl	$⊢ (J \in Comp \land F \in (J Cn K)) \to F : ⋃ J ⟶ ⋃ K$
6	5	ffnd	$⊢ (J \in Comp \land F \in (J Cn K)) \to F Fn ⋃ J$
7		dffn4	$⊢ F Fn ⋃ J \leftrightarrow F : ⋃ J \underset{onto}{⟶} ran F$
8	6 7	sylib	$⊢ (J \in Comp \land F \in (J Cn K)) \to F : ⋃ J \underset{onto}{⟶} ran F$
9		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
10	9	adantl	$⊢ (J \in Comp \land F \in (J Cn K)) \to K \in Top$
11	5	frnd	$⊢ (J \in Comp \land F \in (J Cn K)) \to ran F \subseteq ⋃ K$
12	3	restuni	$⊢ (K \in Top \land ran F \subseteq ⋃ K) \to ran F = ⋃ (K ↾_{𝑡} ran F)$
13	10 11 12	syl2anc	$⊢ (J \in Comp \land F \in (J Cn K)) \to ran F = ⋃ (K ↾_{𝑡} ran F)$
14		foeq3	$⊢ ran F = ⋃ (K ↾_{𝑡} ran F) \to (F : ⋃ J \underset{onto}{⟶} ran F \leftrightarrow F : ⋃ J \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F))$
15	13 14	syl	$⊢ (J \in Comp \land F \in (J Cn K)) \to (F : ⋃ J \underset{onto}{⟶} ran F \leftrightarrow F : ⋃ J \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F))$
16	8 15	mpbid	$⊢ (J \in Comp \land F \in (J Cn K)) \to F : ⋃ J \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F)$
17		simpr	$⊢ (J \in Comp \land F \in (J Cn K)) \to F \in (J Cn K)$
18		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
19	10 18	sylib	$⊢ (J \in Comp \land F \in (J Cn K)) \to K \in TopOn (⋃ K)$
20		ssidd	$⊢ (J \in Comp \land F \in (J Cn K)) \to ran F \subseteq ran F$
21		cnrest2	$⊢ (K \in TopOn (⋃ K) \land ran F \subseteq ran F \land ran F \subseteq ⋃ K) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} ran F)))$
22	19 20 11 21	syl3anc	$⊢ (J \in Comp \land F \in (J Cn K)) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} ran F)))$
23	17 22	mpbid	$⊢ (J \in Comp \land F \in (J Cn K)) \to F \in (J Cn (K ↾_{𝑡} ran F))$
24		eqid	$⊢ ⋃ (K ↾_{𝑡} ran F) = ⋃ (K ↾_{𝑡} ran F)$
25	24	cncmp	$⊢ (J \in Comp \land F : ⋃ J \underset{onto}{⟶} ⋃ (K ↾_{𝑡} ran F) \land F \in (J Cn (K ↾_{𝑡} ran F))) \to K ↾_{𝑡} ran F \in Comp$
26	1 16 23 25	syl3anc	$⊢ (J \in Comp \land F \in (J Cn K)) \to K ↾_{𝑡} ran F \in Comp$

Metamath Proof Explorer

Theorem rncmp

Proof