imafi

Description: Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015)

		Ref	Expression
	Assertion	imafi	$⊢ (Fun F \land X \in Fin) \to F [X] \in Fin$

Step	Hyp	Ref	Expression
1		imadmres	$⊢ F [dom ({F ↾}_{X})] = F [X]$
2		simpr	$⊢ (Fun F \land X \in Fin) \to X \in Fin$
3		dmres	$⊢ dom ({F ↾}_{X}) = X \cap dom F$
4		inss1	$⊢ X \cap dom F \subseteq X$
5	3 4	eqsstri	$⊢ dom ({F ↾}_{X}) \subseteq X$
6		ssfi	$⊢ (X \in Fin \land dom ({F ↾}_{X}) \subseteq X) \to dom ({F ↾}_{X}) \in Fin$
7	2 5 6	sylancl	$⊢ (Fun F \land X \in Fin) \to dom ({F ↾}_{X}) \in Fin$
8		resss	$⊢ {F ↾}_{X} \subseteq F$
9		dmss	$⊢ {F ↾}_{X} \subseteq F \to dom ({F ↾}_{X}) \subseteq dom F$
10	8 9	mp1i	$⊢ (Fun F \land X \in Fin) \to dom ({F ↾}_{X}) \subseteq dom F$
11		fores	$⊢ (Fun F \land dom ({F ↾}_{X}) \subseteq dom F) \to ({F ↾}_{dom ({F ↾}_{X})}) : dom ({F ↾}_{X}) \underset{onto}{⟶} F [dom ({F ↾}_{X})]$
12	10 11	syldan	$⊢ (Fun F \land X \in Fin) \to ({F ↾}_{dom ({F ↾}_{X})}) : dom ({F ↾}_{X}) \underset{onto}{⟶} F [dom ({F ↾}_{X})]$
13		fofi	$⊢ (dom ({F ↾}_{X}) \in Fin \land ({F ↾}_{dom ({F ↾}_{X})}) : dom ({F ↾}_{X}) \underset{onto}{⟶} F [dom ({F ↾}_{X})]) \to F [dom ({F ↾}_{X})] \in Fin$
14	7 12 13	syl2anc	$⊢ (Fun F \land X \in Fin) \to F [dom ({F ↾}_{X})] \in Fin$
15	1 14	eqeltrrid	$⊢ (Fun F \land X \in Fin) \to F [X] \in Fin$

Metamath Proof Explorer