Theorem refrelcoss

Description: The class of cosets by R is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020)

	Ref	Expression
Assertion	refrelcoss	⊢ RefRel ≀ 𝑅

Proof

Step	Hyp	Ref	Expression
1		refrelcoss2	⊢ ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 )
2		dfrefrel2	⊢ ( RefRel ≀ 𝑅 ↔ ( ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ⊆ ≀ 𝑅 ∧ Rel ≀ 𝑅 ) )
3	1 2	mpbir	⊢ RefRel ≀ 𝑅