Theorem dmcoss3

Description: The domain of cosets is the domain of converse. (Contributed by Peter Mazsa, 4-Jan-2019)

	Ref	Expression
Assertion	dmcoss3	⊢ dom ≀ 𝑅 = dom ◡ 𝑅

Proof

Step	Hyp	Ref	Expression
1		dfcoss3	⊢ ≀ 𝑅 = ( 𝑅 ∘ ◡ 𝑅 )
2	1	dmeqi	⊢ dom ≀ 𝑅 = dom ( 𝑅 ∘ ◡ 𝑅 )
3		rncnv	⊢ ran ◡ 𝑅 = dom 𝑅
4	3	eqimssi	⊢ ran ◡ 𝑅 ⊆ dom 𝑅
5		dmcosseq	⊢ ( ran ◡ 𝑅 ⊆ dom 𝑅 → dom ( 𝑅 ∘ ◡ 𝑅 ) = dom ◡ 𝑅 )
6	4 5	ax-mp	⊢ dom ( 𝑅 ∘ ◡ 𝑅 ) = dom ◡ 𝑅
7	2 6	eqtri	⊢ dom ≀ 𝑅 = dom ◡ 𝑅