This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )