Metamath Proof Explorer

Theorem eldisjsdisj

Description: The element of the class of disjoint relations and the disjoint relation predicate are the same, that is ( R e. Disjs <-> Disj R ) when R is a set. (Contributed by Peter Mazsa, 25-Jul-2021)

		Ref	Expression
	Assertion	eldisjsdisj	$⊢ R \in V \to (R \in Disjs \leftrightarrow Disj R)$

Proof

Step	Hyp	Ref	Expression
1		cosscnvex	$⊢ R \in V \to ≀ R^{-1} \in V$
2		elcnvrefrelsrel	$⊢ ≀ R^{-1} \in V \to (≀ R^{-1} \in CnvRefRels \leftrightarrow CnvRefRel ≀ R^{-1})$
3	1 2	syl	$⊢ R \in V \to (≀ R^{-1} \in CnvRefRels \leftrightarrow CnvRefRel ≀ R^{-1})$
4		elrelsrel	$⊢ R \in V \to (R \in Rels \leftrightarrow Rel R)$
5	3 4	anbi12d	$⊢ R \in V \to ((≀ R^{-1} \in CnvRefRels \land R \in Rels) \leftrightarrow (CnvRefRel ≀ R^{-1} \land Rel R))$
6		eldisjs	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \in CnvRefRels \land R \in Rels)$
7		df-disjALTV	$⊢ Disj R \leftrightarrow (CnvRefRel ≀ R^{-1} \land Rel R)$
8	5 6 7	3bitr4g	$⊢ R \in V \to (R \in Disjs \leftrightarrow Disj R)$