Theorem cononrel2

Description: Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020)

	Ref	Expression
Assertion	cononrel2	⊢ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		cnvco	⊢ ◡ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ( ◡ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ∘ ◡ 𝐴 )
2		cnvnonrel	⊢ ◡ ( 𝐵 ∖ ◡ ◡ 𝐵 ) = ∅
3	2	coeq1i	⊢ ( ◡ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ∘ ◡ 𝐴 ) = ( ∅ ∘ ◡ 𝐴 )
4		co01	⊢ ( ∅ ∘ ◡ 𝐴 ) = ∅
5	1 3 4	3eqtri	⊢ ◡ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ∅
6	5	cnveqi	⊢ ◡ ◡ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ◡ ∅
7		relco	⊢ Rel ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) )
8		dfrel2	⊢ ( Rel ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) ↔ ◡ ◡ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) )
9	7 8	mpbi	⊢ ◡ ◡ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) )
10		cnv0	⊢ ◡ ∅ = ∅
11	6 9 10	3eqtr3i	⊢ ( 𝐴 ∘ ( 𝐵 ∖ ◡ ◡ 𝐵 ) ) = ∅