This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfdisjALTV2

Description: Alternate definition of the disjoint relation predicate, cf. dffunALTV2 . (Contributed by Peter Mazsa, 27-Jul-2021)

		Ref	Expression
	Assertion	dfdisjALTV2	$⊢ Disj R \leftrightarrow (≀ R^{-1} \subseteq I \land Rel R)$

Step	Hyp	Ref	Expression
1		df-disjALTV	$⊢ Disj R \leftrightarrow (CnvRefRel ≀ R^{-1} \land Rel R)$
2		cnvrefrelcoss2	$⊢ CnvRefRel ≀ R^{-1} \leftrightarrow ≀ R^{-1} \subseteq I$
3	2	anbi1i	$⊢ (CnvRefRel ≀ R^{-1} \land Rel R) \leftrightarrow (≀ R^{-1} \subseteq I \land Rel R)$
4	1 3	bitri	$⊢ Disj R \leftrightarrow (≀ R^{-1} \subseteq I \land Rel R)$