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 ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )

Proof

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