Theorem wnefimgd

Description: The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	wnefimgd.1	|- ( ph -> A =/= (/) )
	wnefimgd.2	|- ( ph -> F : A --> B )
Assertion	wnefimgd	|- ( ph -> ( F " A ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		wnefimgd.1	|- ( ph -> A =/= (/) )
2		wnefimgd.2	|- ( ph -> F : A --> B )
3		ssid	|- A C_ A
4	2	fdmd	|- ( ph -> dom F = A )
5	3 4	sseqtrrid	|- ( ph -> A C_ dom F )
6		sseqin2	|- ( A C_ dom F <-> ( dom F i^i A ) = A )
7	5 6	sylib	|- ( ph -> ( dom F i^i A ) = A )
8	7 1	eqnetrd	|- ( ph -> ( dom F i^i A ) =/= (/) )
9	8	imadisjlnd	|- ( ph -> ( F " A ) =/= (/) )