Theorem cocnvcnv2

Description: A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007)

	Ref	Expression
Assertion	cocnvcnv2	⊢ ( 𝐴 ∘ ◡ ◡ 𝐵 ) = ( 𝐴 ∘ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	⊢ ◡ ◡ 𝐵 = ( 𝐵 ↾ V )
2	1	coeq2i	⊢ ( 𝐴 ∘ ◡ ◡ 𝐵 ) = ( 𝐴 ∘ ( 𝐵 ↾ V ) )
3		resco	⊢ ( ( 𝐴 ∘ 𝐵 ) ↾ V ) = ( 𝐴 ∘ ( 𝐵 ↾ V ) )
4		relco	⊢ Rel ( 𝐴 ∘ 𝐵 )
5		dfrel3	⊢ ( Rel ( 𝐴 ∘ 𝐵 ) ↔ ( ( 𝐴 ∘ 𝐵 ) ↾ V ) = ( 𝐴 ∘ 𝐵 ) )
6	4 5	mpbi	⊢ ( ( 𝐴 ∘ 𝐵 ) ↾ V ) = ( 𝐴 ∘ 𝐵 )
7	2 3 6	3eqtr2i	⊢ ( 𝐴 ∘ ◡ ◡ 𝐵 ) = ( 𝐴 ∘ 𝐵 )