This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ F Fn A ∧ B ⊆ A → F B = ∅ ↔ B = ∅

Proof

Step Hyp Ref Expression
1 imadisj ⊢ F B = ∅ ↔ dom ⁡ F ∩ B = ∅
2 incom ⊢ dom ⁡ F ∩ B = B ∩ dom ⁡ F
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 3 sseq2d ⊢ F Fn A → B ⊆ dom ⁡ F ↔ B ⊆ A
5 4 biimpar ⊢ F Fn A ∧ B ⊆ A → B ⊆ dom ⁡ F
6 dfss2 ⊢ B ⊆ dom ⁡ F ↔ B ∩ dom ⁡ F = B
7 5 6 sylib ⊢ F Fn A ∧ B ⊆ A → B ∩ dom ⁡ F = B
8 2 7 eqtrid ⊢ F Fn A ∧ B ⊆ A → dom ⁡ F ∩ B = B
9 8 eqeq1d ⊢ F Fn A ∧ B ⊆ A → dom ⁡ F ∩ B = ∅ ↔ B = ∅
10 1 9 bitrid ⊢ F Fn A ∧ B ⊆ A → F B = ∅ ↔ B = ∅