cossssid

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

		Ref	Expression
	Assertion	cossssid	$⊢ ≀ R \subseteq I \leftrightarrow ≀ R \subseteq I \cap (dom ≀ R \times ran ≀ R)$

Step	Hyp	Ref	Expression
1		iss2	$⊢ ≀ R \subseteq I \leftrightarrow ≀ R = I \cap (dom ≀ R \times ran ≀ R)$
2		refrelcoss2	$⊢ (I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \land Rel ≀ R)$
3	2	simpli	$⊢ I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R$
4		eqss	$⊢ ≀ R = I \cap (dom ≀ R \times ran ≀ R) \leftrightarrow (≀ R \subseteq I \cap (dom ≀ R \times ran ≀ R) \land I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R)$
5	3 4	mpbiran2	$⊢ ≀ R = I \cap (dom ≀ R \times ran ≀ R) \leftrightarrow ≀ R \subseteq I \cap (dom ≀ R \times ran ≀ R)$
6	1 5	bitri	$⊢ ≀ R \subseteq I \leftrightarrow ≀ R \subseteq I \cap (dom ≀ R \times ran ≀ R)$

Metamath Proof Explorer