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	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	wnefimgd.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	wnefimgd	⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		wnefimgd.1	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2		wnefimgd.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
3		ssid	⊢ 𝐴 ⊆ 𝐴
4	2	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
5	3 4	sseqtrrid	⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
6		sseqin2	⊢ ( 𝐴 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝐴 ) = 𝐴 )
7	5 6	sylib	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝐴 ) = 𝐴 )
8	7 1	eqnetrd	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝐴 ) ≠ ∅ )
9	8	imadisjlnd	⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ≠ ∅ )