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 = (/) )