Step |
Hyp |
Ref |
Expression |
1 |
|
orc |
|- ( -. A e. dom F -> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) ) |
2 |
|
ianor |
|- ( -. ( A e. dom F /\ Fun ( F |` { A } ) ) <-> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) ) |
3 |
|
df-dfat |
|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) ) |
4 |
2 3
|
xchnxbir |
|- ( -. F defAt A <-> ( -. A e. dom F \/ -. Fun ( F |` { A } ) ) ) |
5 |
1 4
|
sylibr |
|- ( -. A e. dom F -> -. F defAt A ) |
6 |
|
ndfatafv2nrn |
|- ( -. F defAt A -> ( F '''' A ) e/ ran F ) |
7 |
5 6
|
syl |
|- ( -. A e. dom F -> ( F '''' A ) e/ ran F ) |