Definition df-funALTV

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	$$⊢FunALTVF\leftrightarrow \left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1	0	wfunALTV	$$wffFunALTVF$$
2	0	ccoss	$$class\wr F$$
3	2	wcnvrefrel	$$wffCnvRefRel\wr F$$
4	0	wrel	$$wff\mathrm{Rel}F$$
5	3 4	wa	$$wff\left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)$$
6	1 5	wb	$$wff\left(FunALTVF\leftrightarrow \left(CnvRefRel\wr F\wedge \mathrm{Rel}F\right)\right)$$