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	|- ( ( A e. Fin /\ Fun F ) -> ( F " A ) ~<_ A )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( F " A ) = ran ( F |` A )
2		funfn	|- ( Fun F <-> F Fn dom F )
3		resfnfinfin	|- ( ( F Fn dom F /\ A e. Fin ) -> ( F |` A ) e. Fin )
4	2 3	sylanb	|- ( ( Fun F /\ A e. Fin ) -> ( F |` A ) e. Fin )
5		dmfi	|- ( ( F |` A ) e. Fin -> dom ( F |` A ) e. Fin )
6	4 5	syl	|- ( ( Fun F /\ A e. Fin ) -> dom ( F |` A ) e. Fin )
7		funres	|- ( Fun F -> Fun ( F |` A ) )
8		funforn	|- ( Fun ( F |` A ) <-> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
9	7 8	sylib	|- ( Fun F -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
10	9	adantr	|- ( ( Fun F /\ A e. Fin ) -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
11		fodomfi	|- ( ( dom ( F |` A ) e. Fin /\ ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) ) -> ran ( F |` A ) ~<_ dom ( F |` A ) )
12	6 10 11	syl2anc	|- ( ( Fun F /\ A e. Fin ) -> ran ( F |` A ) ~<_ dom ( F |` A ) )
13	1 12	eqbrtrid	|- ( ( Fun F /\ A e. Fin ) -> ( F " A ) ~<_ dom ( F |` A ) )
14		resdmss	|- dom ( F |` A ) C_ A
15		ssdomfi	|- ( A e. Fin -> ( dom ( F |` A ) C_ A -> dom ( F |` A ) ~<_ A ) )
16	14 15	mpi	|- ( A e. Fin -> dom ( F |` A ) ~<_ A )
17		domtr	|- ( ( ( F " A ) ~<_ dom ( F |` A ) /\ dom ( F |` A ) ~<_ A ) -> ( F " A ) ~<_ A )
18	16 17	sylan2	|- ( ( ( F " A ) ~<_ dom ( F |` A ) /\ A e. Fin ) -> ( F " A ) ~<_ A )
19	13 18	sylancom	|- ( ( Fun F /\ A e. Fin ) -> ( F " A ) ~<_ A )
20	19	ancoms	|- ( ( A e. Fin /\ Fun F ) -> ( F " A ) ~<_ A )