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 ) |