Theorem imafi

Description: Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		imaeq2	⊢ ( 𝑥 = ∅ → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ∅ ) )
2	1	eleq1d	⊢ ( 𝑥 = ∅ → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ ∅ ) ∈ Fin ) )
3	2	imbi2d	⊢ ( 𝑥 = ∅ → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ ∅ ) ∈ Fin ) ) )
4		imaeq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑦 ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ 𝑦 ) ∈ Fin ) )
6	5	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ 𝑦 ) ∈ Fin ) ) )
7		imaeq2	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) )
8	7	eleq1d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
9	8	imbi2d	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
10		imaeq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑋 ) )
11	10	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 “ 𝑥 ) ∈ Fin ↔ ( 𝐹 “ 𝑋 ) ∈ Fin ) )
12	11	imbi2d	⊢ ( 𝑥 = 𝑋 → ( ( Fun 𝐹 → ( 𝐹 “ 𝑥 ) ∈ Fin ) ↔ ( Fun 𝐹 → ( 𝐹 “ 𝑋 ) ∈ Fin ) ) )
13		ima0	⊢ ( 𝐹 “ ∅ ) = ∅
14		0fin	⊢ ∅ ∈ Fin
15	13 14	eqeltri	⊢ ( 𝐹 “ ∅ ) ∈ Fin
16	15	a1i	⊢ ( Fun 𝐹 → ( 𝐹 “ ∅ ) ∈ Fin )
17		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
18		fnsnfv	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝑧 ) } = ( 𝐹 “ { 𝑧 } ) )
19	17 18	sylanb	⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝑧 ) } = ( 𝐹 “ { 𝑧 } ) )
20		snfi	⊢ { ( 𝐹 ‘ 𝑧 ) } ∈ Fin
21	19 20	eqeltrrdi	⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
22		ndmima	⊢ ( ¬ 𝑧 ∈ dom 𝐹 → ( 𝐹 “ { 𝑧 } ) = ∅ )
23	22 14	eqeltrdi	⊢ ( ¬ 𝑧 ∈ dom 𝐹 → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
24	23	adantl	⊢ ( ( Fun 𝐹 ∧ ¬ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
25	21 24	pm2.61dan	⊢ ( Fun 𝐹 → ( 𝐹 “ { 𝑧 } ) ∈ Fin )
26		imaundi	⊢ ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐹 “ 𝑦 ) ∪ ( 𝐹 “ { 𝑧 } ) )
27		unfi	⊢ ( ( ( 𝐹 “ 𝑦 ) ∈ Fin ∧ ( 𝐹 “ { 𝑧 } ) ∈ Fin ) → ( ( 𝐹 “ 𝑦 ) ∪ ( 𝐹 “ { 𝑧 } ) ) ∈ Fin )
28	26 27	eqeltrid	⊢ ( ( ( 𝐹 “ 𝑦 ) ∈ Fin ∧ ( 𝐹 “ { 𝑧 } ) ∈ Fin ) → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
29	25 28	sylan2	⊢ ( ( ( 𝐹 “ 𝑦 ) ∈ Fin ∧ Fun 𝐹 ) → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin )
30	29	expcom	⊢ ( Fun 𝐹 → ( ( 𝐹 “ 𝑦 ) ∈ Fin → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
31	30	a2i	⊢ ( ( Fun 𝐹 → ( 𝐹 “ 𝑦 ) ∈ Fin ) → ( Fun 𝐹 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) )
32	31	a1i	⊢ ( 𝑦 ∈ Fin → ( ( Fun 𝐹 → ( 𝐹 “ 𝑦 ) ∈ Fin ) → ( Fun 𝐹 → ( 𝐹 “ ( 𝑦 ∪ { 𝑧 } ) ) ∈ Fin ) ) )
33	3 6 9 12 16 32	findcard2	⊢ ( 𝑋 ∈ Fin → ( Fun 𝐹 → ( 𝐹 “ 𝑋 ) ∈ Fin ) )
34	33	impcom	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ Fin ) → ( 𝐹 “ 𝑋 ) ∈ Fin )