dffunALTV5

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV5 . (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	dffunALTV5	$⊢ FunALTV F \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land Rel F)$

Step	Hyp	Ref	Expression
1		dffunALTV2	$⊢ FunALTV F \leftrightarrow (≀ F \subseteq I \land Rel F)$
2		cossssid5	$⊢ ≀ F \subseteq I \leftrightarrow \forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset)$
3	2	anbi1i	$⊢ (≀ F \subseteq I \land Rel F) \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land Rel F)$
4	1 3	bitri	$⊢ FunALTV F \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land Rel F)$

Metamath Proof Explorer