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

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
2	1	oveq2i	$⊢ K ↾_{𝑡} F [A] = K ↾_{𝑡} ran ({F ↾}_{A})$
3		simpr	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to J ↾_{𝑡} A \in Comp$
4		simpl	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to F \in (J Cn K)$
5		inss2	$⊢ A \cap ⋃ J \subseteq ⋃ J$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	6	cnrest	$⊢ (F \in (J Cn K) \land A \cap ⋃ J \subseteq ⋃ J) \to {F ↾}_{(A \cap ⋃ J)} \in ((J ↾_{𝑡} (A \cap ⋃ J)) Cn K)$
8	4 5 7	sylancl	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to {F ↾}_{(A \cap ⋃ J)} \in ((J ↾_{𝑡} (A \cap ⋃ J)) Cn K)$
9		resdmres	$⊢ {F ↾}_{dom ({F ↾}_{A})} = {F ↾}_{A}$
10		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
11		eqid	$⊢ ⋃ K = ⋃ K$
12	6 11	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
13		fdm	$⊢ F : ⋃ J ⟶ ⋃ K \to dom F = ⋃ J$
14	4 12 13	3syl	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to dom F = ⋃ J$
15	14	ineq2d	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to A \cap dom F = A \cap ⋃ J$
16	10 15	syl5eq	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to dom ({F ↾}_{A}) = A \cap ⋃ J$
17	16	reseq2d	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to {F ↾}_{dom ({F ↾}_{A})} = {F ↾}_{(A \cap ⋃ J)}$
18	9 17	eqtr3id	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to {F ↾}_{A} = {F ↾}_{(A \cap ⋃ J)}$
19		cmptop	$⊢ J ↾_{𝑡} A \in Comp \to J ↾_{𝑡} A \in Top$
20	19	adantl	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to J ↾_{𝑡} A \in Top$
21		restrcl	$⊢ J ↾_{𝑡} A \in Top \to (J \in V \land A \in V)$
22	6	restin	$⊢ (J \in V \land A \in V) \to J ↾_{𝑡} A = J ↾_{𝑡} (A \cap ⋃ J)$
23	20 21 22	3syl	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to J ↾_{𝑡} A = J ↾_{𝑡} (A \cap ⋃ J)$
24	23	oveq1d	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to (J ↾_{𝑡} A) Cn K = (J ↾_{𝑡} (A \cap ⋃ J)) Cn K$
25	8 18 24	3eltr4d	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)$
26		rncmp	$⊢ (J ↾_{𝑡} A \in Comp \land {F ↾}_{A} \in ((J ↾_{𝑡} A) Cn K)) \to K ↾_{𝑡} ran ({F ↾}_{A}) \in Comp$
27	3 25 26	syl2anc	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to K ↾_{𝑡} ran ({F ↾}_{A}) \in Comp$
28	2 27	eqeltrid	$⊢ (F \in (J Cn K) \land J ↾_{𝑡} A \in Comp) \to K ↾_{𝑡} F [A] \in Comp$

Metamath Proof Explorer

Theorem imacmp

Proof