Metamath Proof Explorer

Theorem fdomne0

Description: A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion fdomne0 
|- ( ( F : X --> Y /\ X =/= (/) ) -> ( F =/= (/) /\ Y =/= (/) ) )

Proof

Step Hyp Ref Expression
1 f0dom0 
 |-  ( F : X --> Y -> ( X = (/) <-> F = (/) ) )
2 1 necon3bid 
 |-  ( F : X --> Y -> ( X =/= (/) <-> F =/= (/) ) )
3 2 biimpa 
 |-  ( ( F : X --> Y /\ X =/= (/) ) -> F =/= (/) )
4 feq3 
 |-  ( Y = (/) -> ( F : X --> Y <-> F : X --> (/) ) )
5 f00 
 |-  ( F : X --> (/) <-> ( F = (/) /\ X = (/) ) )
6 5 simprbi 
 |-  ( F : X --> (/) -> X = (/) )
7 4 6 biimtrdi 
 |-  ( Y = (/) -> ( F : X --> Y -> X = (/) ) )
8 nne 
 |-  ( -. X =/= (/) <-> X = (/) )
9 7 8 imbitrrdi 
 |-  ( Y = (/) -> ( F : X --> Y -> -. X =/= (/) ) )
10 imnan 
 |-  ( ( F : X --> Y -> -. X =/= (/) ) <-> -. ( F : X --> Y /\ X =/= (/) ) )
11 9 10 sylib 
 |-  ( Y = (/) -> -. ( F : X --> Y /\ X =/= (/) ) )
12 11 necon2ai 
 |-  ( ( F : X --> Y /\ X =/= (/) ) -> Y =/= (/) )
13 3 12 jca 
 |-  ( ( F : X --> Y /\ X =/= (/) ) -> ( F =/= (/) /\ Y =/= (/) ) )