Metamath Proof Explorer

Theorem f00

Description: A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003)

Ref Expression
Assertion f00 
|- ( F : A --> (/) <-> ( F = (/) /\ A = (/) ) )

Proof

Step Hyp Ref Expression
1 ffun 
 |-  ( F : A --> (/) -> Fun F )
2 frn 
 |-  ( F : A --> (/) -> ran F C_ (/) )
3 ss0 
 |-  ( ran F C_ (/) -> ran F = (/) )
4 2 3 syl 
 |-  ( F : A --> (/) -> ran F = (/) )
5 dm0rn0 
 |-  ( dom F = (/) <-> ran F = (/) )
6 4 5 sylibr 
 |-  ( F : A --> (/) -> dom F = (/) )
7 df-fn 
 |-  ( F Fn (/) <-> ( Fun F /\ dom F = (/) ) )
8 1 6 7 sylanbrc 
 |-  ( F : A --> (/) -> F Fn (/) )
9 fn0 
 |-  ( F Fn (/) <-> F = (/) )
10 8 9 sylib 
 |-  ( F : A --> (/) -> F = (/) )
11 fdm 
 |-  ( F : A --> (/) -> dom F = A )
12 11 6 eqtr3d 
 |-  ( F : A --> (/) -> A = (/) )
13 10 12 jca 
 |-  ( F : A --> (/) -> ( F = (/) /\ A = (/) ) )
14 f0 
 |-  (/) : (/) --> (/)
15 feq1 
 |-  ( F = (/) -> ( F : A --> (/) <-> (/) : A --> (/) ) )
16 feq2 
 |-  ( A = (/) -> ( (/) : A --> (/) <-> (/) : (/) --> (/) ) )
17 15 16 sylan9bb 
 |-  ( ( F = (/) /\ A = (/) ) -> ( F : A --> (/) <-> (/) : (/) --> (/) ) )
18 14 17 mpbiri 
 |-  ( ( F = (/) /\ A = (/) ) -> F : A --> (/) )
19 13 18 impbii 
 |-  ( F : A --> (/) <-> ( F = (/) /\ A = (/) ) )