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 \leftrightarrow Fun F$

Proof

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

Metamath Proof Explorer

Theorem funALTVfun

Proof