Step |
Hyp |
Ref |
Expression |
1 |
|
suppval1 |
|- ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { x e. dom F | ( F ` x ) =/= Z } ) |
2 |
1
|
adantr |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( F supp Z ) = { x e. dom F | ( F ` x ) =/= Z } ) |
3 |
|
df-nel |
|- ( Z e/ ran F <-> -. Z e. ran F ) |
4 |
|
fvelrn |
|- ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F ) |
5 |
4
|
3ad2antl1 |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( F ` x ) e. ran F ) |
6 |
|
eleq1 |
|- ( Z = ( F ` x ) -> ( Z e. ran F <-> ( F ` x ) e. ran F ) ) |
7 |
6
|
eqcoms |
|- ( ( F ` x ) = Z -> ( Z e. ran F <-> ( F ` x ) e. ran F ) ) |
8 |
5 7
|
syl5ibrcom |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( ( F ` x ) = Z -> Z e. ran F ) ) |
9 |
8
|
necon3bd |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( -. Z e. ran F -> ( F ` x ) =/= Z ) ) |
10 |
3 9
|
syl5bi |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ x e. dom F ) -> ( Z e/ ran F -> ( F ` x ) =/= Z ) ) |
11 |
10
|
impancom |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( x e. dom F -> ( F ` x ) =/= Z ) ) |
12 |
11
|
ralrimiv |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> A. x e. dom F ( F ` x ) =/= Z ) |
13 |
|
rabid2 |
|- ( dom F = { x e. dom F | ( F ` x ) =/= Z } <-> A. x e. dom F ( F ` x ) =/= Z ) |
14 |
12 13
|
sylibr |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> dom F = { x e. dom F | ( F ` x ) =/= Z } ) |
15 |
2 14
|
eqtr4d |
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( F supp Z ) = dom F ) |