Metamath Proof Explorer


Theorem funALTVfun

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 )

Proof

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 )