refrelcoss2

Description: The class of cosets by R is reflexive, see dfrefrel2 . (Contributed by Peter Mazsa, 30-Jul-2019)

		Ref	Expression
	Assertion	refrelcoss2	$⊢ (I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \land Rel ≀ R)$

Step	Hyp	Ref	Expression
1		refrelcoss3	$⊢ (\forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y) \land Rel ≀ R)$
2		idinxpss	$⊢ I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \leftrightarrow \forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y)$
3	2	anbi1i	$⊢ (I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \land Rel ≀ R) \leftrightarrow (\forall x \in dom ≀ R \forall y \in ran ≀ R (x = y \to x ≀ R y) \land Rel ≀ R)$
4	1 3	mpbir	$⊢ (I \cap (dom ≀ R \times ran ≀ R) \subseteq ≀ R \land Rel ≀ R)$

Metamath Proof Explorer