Metamath Proof Explorer

Theorem f0rn0

Description: If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018)

Ref Expression
Assertion f0rn0 
|- ( ( E : X --> Y /\ -. E. y e. Y y e. ran E ) -> X = (/) )

Proof

Step Hyp Ref Expression
1 fdm 
 |-  ( E : X --> Y -> dom E = X )
2 frn 
 |-  ( E : X --> Y -> ran E C_ Y )
3 ralnex 
 |-  ( A. y e. Y -. y e. ran E <-> -. E. y e. Y y e. ran E )
4 disj 
 |-  ( ( Y i^i ran E ) = (/) <-> A. y e. Y -. y e. ran E )
5 dfss2 
 |-  ( ran E C_ Y <-> ( ran E i^i Y ) = ran E )
6 incom 
 |-  ( ran E i^i Y ) = ( Y i^i ran E )
7 6 eqeq1i 
 |-  ( ( ran E i^i Y ) = ran E <-> ( Y i^i ran E ) = ran E )
8 eqtr2 
 |-  ( ( ( Y i^i ran E ) = ran E /\ ( Y i^i ran E ) = (/) ) -> ran E = (/) )
9 8 ex 
 |-  ( ( Y i^i ran E ) = ran E -> ( ( Y i^i ran E ) = (/) -> ran E = (/) ) )
10 7 9 sylbi 
 |-  ( ( ran E i^i Y ) = ran E -> ( ( Y i^i ran E ) = (/) -> ran E = (/) ) )
11 5 10 sylbi 
 |-  ( ran E C_ Y -> ( ( Y i^i ran E ) = (/) -> ran E = (/) ) )
12 4 11 biimtrrid 
 |-  ( ran E C_ Y -> ( A. y e. Y -. y e. ran E -> ran E = (/) ) )
13 3 12 biimtrrid 
 |-  ( ran E C_ Y -> ( -. E. y e. Y y e. ran E -> ran E = (/) ) )
14 2 13 syl 
 |-  ( E : X --> Y -> ( -. E. y e. Y y e. ran E -> ran E = (/) ) )
15 14 imp 
 |-  ( ( E : X --> Y /\ -. E. y e. Y y e. ran E ) -> ran E = (/) )
16 15 adantl 
 |-  ( ( dom E = X /\ ( E : X --> Y /\ -. E. y e. Y y e. ran E ) ) -> ran E = (/) )
17 dm0rn0 
 |-  ( dom E = (/) <-> ran E = (/) )
18 16 17 sylibr 
 |-  ( ( dom E = X /\ ( E : X --> Y /\ -. E. y e. Y y e. ran E ) ) -> dom E = (/) )
19 eqeq1 
 |-  ( X = dom E -> ( X = (/) <-> dom E = (/) ) )
20 19 eqcoms 
 |-  ( dom E = X -> ( X = (/) <-> dom E = (/) ) )
21 20 adantr 
 |-  ( ( dom E = X /\ ( E : X --> Y /\ -. E. y e. Y y e. ran E ) ) -> ( X = (/) <-> dom E = (/) ) )
22 18 21 mpbird 
 |-  ( ( dom E = X /\ ( E : X --> Y /\ -. E. y e. Y y e. ran E ) ) -> X = (/) )
23 22 exp32 
 |-  ( dom E = X -> ( E : X --> Y -> ( -. E. y e. Y y e. ran E -> X = (/) ) ) )
24 1 23 mpcom 
 |-  ( E : X --> Y -> ( -. E. y e. Y y e. ran E -> X = (/) ) )
25 24 imp 
 |-  ( ( E : X --> Y /\ -. E. y e. Y y e. ran E ) -> X = (/) )