Theorem cnvrefrelcoss2

Description: Necessary and sufficient condition for a coset relation to be a converse reflexive relation. (Contributed by Peter Mazsa, 27-Jul-2021)

	Ref	Expression
Assertion	cnvrefrelcoss2	⊢ ( CnvRefRel ≀ 𝑅 ↔ ≀ 𝑅 ⊆ I )

Proof

Step	Hyp	Ref	Expression
1		relcoss	⊢ Rel ≀ 𝑅
2		dfcnvrefrel2	⊢ ( CnvRefRel ≀ 𝑅 ↔ ( ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) ∧ Rel ≀ 𝑅 ) )
3	1 2	mpbiran2	⊢ ( CnvRefRel ≀ 𝑅 ↔ ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) )
4		cossssid	⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ ( I ∩ ( dom ≀ 𝑅 × ran ≀ 𝑅 ) ) )
5	3 4	bitr4i	⊢ ( CnvRefRel ≀ 𝑅 ↔ ≀ 𝑅 ⊆ I )