dffunsALTV5

Description: Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021)

		Ref	Expression
	Assertion	dffunsALTV5	$⊢ FunsALTV = \{f \in Rels \| \forall x \in ran f \forall y \in ran f (x = y \lor [x] f^{-1} \cap [y] f^{-1} = \emptyset)\}$

Step	Hyp	Ref	Expression
1		dffunsALTV4	$⊢ FunsALTV = \{f \in Rels \| \forall u \exists^{*} x u f x\}$
2		ineccnvmo2	$⊢ \forall x \in ran f \forall y \in ran f (x = y \lor [x] f^{-1} \cap [y] f^{-1} = \emptyset) \leftrightarrow \forall u \exists^{*} x u f x$
3	2	rabbii	$⊢ \{f \in Rels \| \forall x \in ran f \forall y \in ran f (x = y \lor [x] f^{-1} \cap [y] f^{-1} = \emptyset)\} = \{f \in Rels \| \forall u \exists^{*} x u f x\}$
4	1 3	eqtr4i	$⊢ FunsALTV = \{f \in Rels \| \forall x \in ran f \forall y \in ran f (x = y \lor [x] f^{-1} \cap [y] f^{-1} = \emptyset)\}$

Metamath Proof Explorer