Theorem imadomfi

Description: An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025)

	Ref	Expression
Assertion	imadomfi	⊢ ( ( 𝐴 ∈ Fin ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
2		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
3		resfnfinfin	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) ∈ Fin )
4	2 3	sylanb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) ∈ Fin )
5		dmfi	⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ Fin → dom ( 𝐹 ↾ 𝐴 ) ∈ Fin )
6	4 5	syl	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ Fin ) → dom ( 𝐹 ↾ 𝐴 ) ∈ Fin )
7		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
8		funforn	⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
9	7 8	sylib	⊢ ( Fun 𝐹 → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
10	9	adantr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ Fin ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) )
11		fodomfi	⊢ ( ( dom ( 𝐹 ↾ 𝐴 ) ∈ Fin ∧ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) –onto→ ran ( 𝐹 ↾ 𝐴 ) ) → ran ( 𝐹 ↾ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) )
12	6 10 11	syl2anc	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ Fin ) → ran ( 𝐹 ↾ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) )
13	1 12	eqbrtrid	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ Fin ) → ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) )
14		resdmss	⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴
15		ssdomfi	⊢ ( 𝐴 ∈ Fin → ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 → dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 ) )
16	14 15	mpi	⊢ ( 𝐴 ∈ Fin → dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 )
17		domtr	⊢ ( ( ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) ≼ 𝐴 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
18	16 17	sylan2	⊢ ( ( ( 𝐹 “ 𝐴 ) ≼ dom ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ∈ Fin ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
19	13 18	sylancom	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ Fin ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
20	19	ancoms	⊢ ( ( 𝐴 ∈ Fin ∧ Fun 𝐹 ) → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )