Description: Define the function relation predicate, i.e., the function predicate. This definition of the function predicate (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same, that is ( FunALTV F <-> Fun F ) , see funALTVfun .
The element of the class of functions and the function predicate are the same, that is ( F e. FunsALTV <-> FunALTV F ) when F is a set, see elfunsALTVfunALTV . Alternate definitions are dffunALTV2 , ... , dffunALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-funALTV | |- ( FunALTV F <-> ( CnvRefRel ,~ F /\ Rel F ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | |- F |
|
| 1 | 0 | wfunALTV | |- FunALTV F |
| 2 | 0 | ccoss | |- ,~ F |
| 3 | 2 | wcnvrefrel | |- CnvRefRel ,~ F |
| 4 | 0 | wrel | |- Rel F |
| 5 | 3 4 | wa | |- ( CnvRefRel ,~ F /\ Rel F ) |
| 6 | 1 5 | wb | |- ( FunALTV F <-> ( CnvRefRel ,~ F /\ Rel F ) ) |