dffunsALTV2

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

		Ref	Expression
	Assertion	dffunsALTV2	$⊢ FunsALTV = \{f \in Rels \| ≀ f \subseteq I\}$

Step	Hyp	Ref	Expression
1		dffunsALTV	$⊢ FunsALTV = \{f \in Rels \| ≀ f \in CnvRefRels\}$
2		cosselcnvrefrels2	$⊢ ≀ f \in CnvRefRels \leftrightarrow (≀ f \subseteq I \land ≀ f \in Rels)$
3		cosselrels	$⊢ f \in Rels \to ≀ f \in Rels$
4	3	biantrud	$⊢ f \in Rels \to (≀ f \subseteq I \leftrightarrow (≀ f \subseteq I \land ≀ f \in Rels))$
5	2 4	bitr4id	$⊢ f \in Rels \to (≀ f \in CnvRefRels \leftrightarrow ≀ f \subseteq I)$
6	1 5	rabimbieq	$⊢ FunsALTV = \{f \in Rels \| ≀ f \subseteq I\}$

Metamath Proof Explorer