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

Metamath Proof Explorer

Theorem fn0

Description: A function with empty domain is empty. (Contributed by NM, 15-Apr-1998) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fn0 ⊢ F Fn ∅ ↔ F = ∅

Proof

Step Hyp Ref Expression
1 fnrel ⊢ F Fn ∅ → Rel ⁡ F
2 fndm ⊢ F Fn ∅ → dom ⁡ F = ∅
3 reldm0 ⊢ Rel ⁡ F → F = ∅ ↔ dom ⁡ F = ∅
4 3 biimpar ⊢ Rel ⁡ F ∧ dom ⁡ F = ∅ → F = ∅
5 1 2 4 syl2anc ⊢ F Fn ∅ → F = ∅
6 fun0 ⊢ Fun ⁡ ∅
7 dm0 ⊢ dom ⁡ ∅ = ∅
8 df-fn ⊢ ∅ Fn ∅ ↔ Fun ⁡ ∅ ∧ dom ⁡ ∅ = ∅
9 6 7 8 mpbir2an ⊢ ∅ Fn ∅
10 fneq1 ⊢ F = ∅ → F Fn ∅ ↔ ∅ Fn ∅
11 9 10 mpbiri ⊢ F = ∅ → F Fn ∅
12 5 11 impbii ⊢ F Fn ∅ ↔ F = ∅