Metamath Proof Explorer

Theorem fo00

Description: Onto mapping of the empty set. (Contributed by NM, 22-Mar-2006)

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

Proof

Step Hyp Ref Expression
1 fofn 
 |-  ( F : (/) -onto-> A -> F Fn (/) )
2 fn0 
 |-  ( F Fn (/) <-> F = (/) )
3 f10 
 |-  (/) : (/) -1-1-> A
4 f1eq1 
 |-  ( F = (/) -> ( F : (/) -1-1-> A <-> (/) : (/) -1-1-> A ) )
5 3 4 mpbiri 
 |-  ( F = (/) -> F : (/) -1-1-> A )
6 2 5 sylbi 
 |-  ( F Fn (/) -> F : (/) -1-1-> A )
7 1 6 syl 
 |-  ( F : (/) -onto-> A -> F : (/) -1-1-> A )
8 7 ancri 
 |-  ( F : (/) -onto-> A -> ( F : (/) -1-1-> A /\ F : (/) -onto-> A ) )
9 df-f1o 
 |-  ( F : (/) -1-1-onto-> A <-> ( F : (/) -1-1-> A /\ F : (/) -onto-> A ) )
10 8 9 sylibr 
 |-  ( F : (/) -onto-> A -> F : (/) -1-1-onto-> A )
11 f1ofo 
 |-  ( F : (/) -1-1-onto-> A -> F : (/) -onto-> A )
12 10 11 impbii 
 |-  ( F : (/) -onto-> A <-> F : (/) -1-1-onto-> A )
13 f1o00 
 |-  ( F : (/) -1-1-onto-> A <-> ( F = (/) /\ A = (/) ) )
14 12 13 bitri 
 |-  ( F : (/) -onto-> A <-> ( F = (/) /\ A = (/) ) )