Step |
Hyp |
Ref |
Expression |
1 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
2 |
|
fnafv2elrn |
|- ( ( F Fn A /\ C e. A ) -> ( F '''' C ) e. ran F ) |
3 |
1 2
|
sylan |
|- ( ( F : A --> B /\ C e. A ) -> ( F '''' C ) e. ran F ) |
4 |
3
|
ex |
|- ( F : A --> B -> ( C e. A -> ( F '''' C ) e. ran F ) ) |
5 |
|
fdm |
|- ( F : A --> B -> dom F = A ) |
6 |
|
ndmafv2nrn |
|- ( -. C e. dom F -> ( F '''' C ) e/ ran F ) |
7 |
|
df-nel |
|- ( ( F '''' C ) e/ ran F <-> -. ( F '''' C ) e. ran F ) |
8 |
6 7
|
sylib |
|- ( -. C e. dom F -> -. ( F '''' C ) e. ran F ) |
9 |
8
|
con4i |
|- ( ( F '''' C ) e. ran F -> C e. dom F ) |
10 |
|
eleq2 |
|- ( dom F = A -> ( C e. dom F <-> C e. A ) ) |
11 |
9 10
|
syl5ib |
|- ( dom F = A -> ( ( F '''' C ) e. ran F -> C e. A ) ) |
12 |
5 11
|
syl |
|- ( F : A --> B -> ( ( F '''' C ) e. ran F -> C e. A ) ) |
13 |
4 12
|
impbid |
|- ( F : A --> B -> ( C e. A <-> ( F '''' C ) e. ran F ) ) |