Theorem imadomg

Description: An image of a function under a set is dominated by the set. Proposition 10.34 of TakeutiZaring p. 92. (Contributed by NM, 23-Jul-2004)

	Ref	Expression
Assertion	imadomg	|- ( A e. B -> ( Fun F -> ( F " A ) ~<_ A ) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( F " A ) = ran ( F |` A )
2		resfunexg	|- ( ( Fun F /\ A e. B ) -> ( F |` A ) e. _V )
3	2	dmexd	|- ( ( Fun F /\ A e. B ) -> dom ( F |` A ) e. _V )
4		funres	|- ( Fun F -> Fun ( F |` A ) )
5		funforn	|- ( Fun ( F |` A ) <-> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
6	4 5	sylib	|- ( Fun F -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
7	6	adantr	|- ( ( Fun F /\ A e. B ) -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
8		fodomg	|- ( dom ( F |` A ) e. _V -> ( ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) -> ran ( F |` A ) ~<_ dom ( F |` A ) ) )
9	3 7 8	sylc	|- ( ( Fun F /\ A e. B ) -> ran ( F |` A ) ~<_ dom ( F |` A ) )
10	1 9	eqbrtrid	|- ( ( Fun F /\ A e. B ) -> ( F " A ) ~<_ dom ( F |` A ) )
11	10	expcom	|- ( A e. B -> ( Fun F -> ( F " A ) ~<_ dom ( F |` A ) ) )
12		dmres	|- dom ( F |` A ) = ( A i^i dom F )
13		inss1	|- ( A i^i dom F ) C_ A
14	12 13	eqsstri	|- dom ( F |` A ) C_ A
15		ssdomg	|- ( A e. B -> ( dom ( F |` A ) C_ A -> dom ( F |` A ) ~<_ A ) )
16	14 15	mpi	|- ( A e. B -> 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. B ) -> ( F " A ) ~<_ A )
19	18	expcom	|- ( A e. B -> ( ( F " A ) ~<_ dom ( F |` A ) -> ( F " A ) ~<_ A ) )
20	11 19	syld	|- ( A e. B -> ( Fun F -> ( F " A ) ~<_ A ) )