Theorem fnimaeq0

Description: Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 . (Contributed by Stefan O'Rear, 21-Jan-2015)

	Ref	Expression
Assertion	fnimaeq0	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 “ 𝐵 ) = ∅ ↔ 𝐵 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		imadisj	⊢ ( ( 𝐹 “ 𝐵 ) = ∅ ↔ ( dom 𝐹 ∩ 𝐵 ) = ∅ )
2		incom	⊢ ( dom 𝐹 ∩ 𝐵 ) = ( 𝐵 ∩ dom 𝐹 )
3		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
4	3	sseq2d	⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
5	4	biimpar	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ dom 𝐹 )
6		dfss2	⊢ ( 𝐵 ⊆ dom 𝐹 ↔ ( 𝐵 ∩ dom 𝐹 ) = 𝐵 )
7	5 6	sylib	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ∩ dom 𝐹 ) = 𝐵 )
8	2 7	eqtrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( dom 𝐹 ∩ 𝐵 ) = 𝐵 )
9	8	eqeq1d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( dom 𝐹 ∩ 𝐵 ) = ∅ ↔ 𝐵 = ∅ ) )
10	1 9	bitrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝐹 “ 𝐵 ) = ∅ ↔ 𝐵 = ∅ ) )