elfunsALTV5

Description: Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021)

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

Step	Hyp	Ref	Expression
1		elfunsALTV	$⊢ F \in FunsALTV \leftrightarrow (≀ F \in CnvRefRels \land F \in Rels)$
2		cosselcnvrefrels5	$⊢ ≀ F \in CnvRefRels \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land ≀ F \in Rels)$
3		cosselrels	$⊢ F \in Rels \to ≀ F \in Rels$
4	3	biantrud	$⊢ F \in Rels \to (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land ≀ F \in Rels))$
5	2 4	bitr4id	$⊢ F \in Rels \to (≀ F \in CnvRefRels \leftrightarrow \forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset))$
6	5	pm5.32ri	$⊢ (≀ F \in CnvRefRels \land F \in Rels) \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land F \in Rels)$
7	1 6	bitri	$⊢ F \in FunsALTV \leftrightarrow (\forall x \in ran F \forall y \in ran F (x = y \lor [x] F^{-1} \cap [y] F^{-1} = \emptyset) \land F \in Rels)$

Metamath Proof Explorer