elfunsALTV2

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

		Ref	Expression
	Assertion	elfunsALTV2	$⊢ F \in FunsALTV \leftrightarrow (≀ F \subseteq I \land F \in Rels)$

Step	Hyp	Ref	Expression
1		elfunsALTV	$⊢ F \in FunsALTV \leftrightarrow (≀ F \in CnvRefRels \land F \in Rels)$
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	5	pm5.32ri	$⊢ (≀ F \in CnvRefRels \land F \in Rels) \leftrightarrow (≀ F \subseteq I \land F \in Rels)$
7	1 6	bitri	$⊢ F \in FunsALTV \leftrightarrow (≀ F \subseteq I \land F \in Rels)$

Metamath Proof Explorer