Metamath Proof Explorer


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 df-ss ( 𝐵 ⊆ dom 𝐹 ↔ ( 𝐵 ∩ dom 𝐹 ) = 𝐵 )
7 5 6 sylib ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐵 ∩ dom 𝐹 ) = 𝐵 )
8 2 7 eqtrid ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( dom 𝐹𝐵 ) = 𝐵 )
9 8 eqeq1d ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( dom 𝐹𝐵 ) = ∅ ↔ 𝐵 = ∅ ) )
10 1 9 syl5bb ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ( 𝐹𝐵 ) = ∅ ↔ 𝐵 = ∅ ) )