eldisjs2

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

		Ref	Expression
	Assertion	eldisjs2	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \subseteq I \land R \in Rels)$

Step	Hyp	Ref	Expression
1		eldisjs	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \in CnvRefRels \land R \in Rels)$
2		cosselcnvrefrels2	$⊢ ≀ R^{-1} \in CnvRefRels \leftrightarrow (≀ R^{-1} \subseteq I \land ≀ R^{-1} \in Rels)$
3		cosscnvelrels	$⊢ R \in Rels \to ≀ R^{-1} \in Rels$
4	3	biantrud	$⊢ R \in Rels \to (≀ R^{-1} \subseteq I \leftrightarrow (≀ R^{-1} \subseteq I \land ≀ R^{-1} \in Rels))$
5	2 4	bitr4id	$⊢ R \in Rels \to (≀ R^{-1} \in CnvRefRels \leftrightarrow ≀ R^{-1} \subseteq I)$
6	5	pm5.32ri	$⊢ (≀ R^{-1} \in CnvRefRels \land R \in Rels) \leftrightarrow (≀ R^{-1} \subseteq I \land R \in Rels)$
7	1 6	bitri	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \subseteq I \land R \in Rels)$

Metamath Proof Explorer