Description: Our definition of the function predicate df-funALTV (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | funALTVfun | |- ( FunALTV F <-> Fun F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvrefrelcoss2 | |- ( CnvRefRel ,~ F <-> ,~ F C_ _I ) |
|
| 2 | dfcoss3 | |- ,~ F = ( F o. `' F ) |
|
| 3 | 2 | sseq1i | |- ( ,~ F C_ _I <-> ( F o. `' F ) C_ _I ) |
| 4 | 1 3 | bitri | |- ( CnvRefRel ,~ F <-> ( F o. `' F ) C_ _I ) |
| 5 | 4 | anbi2ci | |- ( ( CnvRefRel ,~ F /\ Rel F ) <-> ( Rel F /\ ( F o. `' F ) C_ _I ) ) |
| 6 | df-funALTV | |- ( FunALTV F <-> ( CnvRefRel ,~ F /\ Rel F ) ) |
|
| 7 | df-fun | |- ( Fun F <-> ( Rel F /\ ( F o. `' F ) C_ _I ) ) |
|
| 8 | 5 6 7 | 3bitr4i | |- ( FunALTV F <-> Fun F ) |