Theorem imafi

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

	Ref	Expression
Assertion	imafi	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 “ 𝑋 ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		imadmres	⊢ ( 𝐹 “ dom ( 𝐹 ↾ 𝑋 ) ) = ( 𝐹 “ 𝑋 )
2		simpr	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → 𝑋 ∈ Fin )
3		dmres	⊢ dom ( 𝐹 ↾ 𝑋 ) = ( 𝑋 ∩ dom 𝐹 )
4		inss1	⊢ ( 𝑋 ∩ dom 𝐹 ) ⊆ 𝑋
5	3 4	eqsstri	⊢ dom ( 𝐹 ↾ 𝑋 ) ⊆ 𝑋
6		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ dom ( 𝐹 ↾ 𝑋 ) ⊆ 𝑋 ) → dom ( 𝐹 ↾ 𝑋 ) ∈ Fin )
7	2 5 6	sylancl	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → dom ( 𝐹 ↾ 𝑋 ) ∈ Fin )
8		resss	⊢ ( 𝐹 ↾ 𝑋 ) ⊆ 𝐹
9		dmss	⊢ ( ( 𝐹 ↾ 𝑋 ) ⊆ 𝐹 → dom ( 𝐹 ↾ 𝑋 ) ⊆ dom 𝐹 )
10	8 9	mp1i	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → dom ( 𝐹 ↾ 𝑋 ) ⊆ dom 𝐹 )
11		fores	⊢ ( ( Fun 𝐹 ∧ dom ( 𝐹 ↾ 𝑋 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –onto→ ( 𝐹 “ dom ( 𝐹 ↾ 𝑋 ) ) )
12	10 11	syldan	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –onto→ ( 𝐹 “ dom ( 𝐹 ↾ 𝑋 ) ) )
13		fofi	⊢ ( ( dom ( 𝐹 ↾ 𝑋 ) ∈ Fin ∧ ( 𝐹 ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –onto→ ( 𝐹 “ dom ( 𝐹 ↾ 𝑋 ) ) ) → ( 𝐹 “ dom ( 𝐹 ↾ 𝑋 ) ) ∈ Fin )
14	7 12 13	syl2anc	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 “ dom ( 𝐹 ↾ 𝑋 ) ) ∈ Fin )
15	1 14	eqeltrrid	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 “ 𝑋 ) ∈ Fin )