Metamath Proof Explorer

Theorem cossssid5

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021)

		Ref	Expression
	Assertion	cossssid5	$⊢ ≀ R \subseteq I \leftrightarrow \forall x \in ran R \forall y \in ran R (x = y \lor [x] R^{-1} \cap [y] R^{-1} = \emptyset)$

Step	Hyp	Ref	Expression
1		cossssid4	$⊢ ≀ R \subseteq I \leftrightarrow \forall u \exists^{*} x u R x$
2		ineccnvmo2	$⊢ \forall x \in ran R \forall y \in ran R (x = y \lor [x] R^{-1} \cap [y] R^{-1} = \emptyset) \leftrightarrow \forall u \exists^{*} x u R x$
3	1 2	bitr4i	$⊢ ≀ R \subseteq I \leftrightarrow \forall x \in ran R \forall y \in ran R (x = y \lor [x] R^{-1} \cap [y] R^{-1} = \emptyset)$