Description: Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mptrcl.1 | |- F = ( x e. A |-> B ) |
|
| Assertion | mptrcl | |- ( I e. ( F ` X ) -> X e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mptrcl.1 | |- F = ( x e. A |-> B ) |
|
| 2 | n0i | |- ( I e. ( F ` X ) -> -. ( F ` X ) = (/) ) |
|
| 3 | 1 | dmmptss | |- dom F C_ A |
| 4 | 3 | sseli | |- ( X e. dom F -> X e. A ) |
| 5 | ndmfv | |- ( -. X e. dom F -> ( F ` X ) = (/) ) |
|
| 6 | 4 5 | nsyl4 | |- ( -. ( F ` X ) = (/) -> X e. A ) |
| 7 | 2 6 | syl | |- ( I e. ( F ` X ) -> X e. A ) |