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	$$⊢FunALTVF\leftrightarrow \mathrm{Fun}F$$

Proof

Step	Hyp	Ref	Expression
1		cnvrefrelcoss2	$$⊢CnvRefRel\wr F\leftrightarrow \wr F\subseteq \mathrm{I}$$
2		dfcoss3	$$⊢\wr F=F\circ F^{-1}$$
3	2	sseq1i	$$⊢\wr F\subseteq \mathrm{I}\leftrightarrow F\circ F^{-1}\subseteq \mathrm{I}$$
4	1 3	bitri	$$⊢CnvRefRel\wr F\leftrightarrow F\circ F^{-1}\subseteq \mathrm{I}$$
5	4	anbi2ci	$$⊢\left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)\leftrightarrow \left(\mathrm{Rel}F\wedge F\circ F^{-1}\subseteq \mathrm{I}\right)$$
6		df-funALTV	$$⊢FunALTVF\leftrightarrow \left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)$$
7		df-fun	$$⊢\mathrm{Fun}F\leftrightarrow \left(\mathrm{Rel}F\wedge F\circ F^{-1}\subseteq \mathrm{I}\right)$$
8	5 6 7	3bitr4i	$$⊢FunALTVF\leftrightarrow \mathrm{Fun}F$$