Description: Function value when F is (locally) not a function. Theorem 6.12(2) of TakeutiZaring p. 27, analogous to tz6.12-2 . (Contributed by AV, 5-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tz6.12-2-afv2 | |- ( -. E! x A F x -> ( F '''' A ) e/ ran F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfdfat2 | |- ( F defAt A <-> ( A e. dom F /\ E! x A F x ) ) |
|
| 2 | 1 | simprbi | |- ( F defAt A -> E! x A F x ) |
| 3 | ndfatafv2nrn | |- ( -. F defAt A -> ( F '''' A ) e/ ran F ) |
|
| 4 | 2 3 | nsyl5 | |- ( -. E! x A F x -> ( F '''' A ) e/ ran F ) |