Theorem cononrel1

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

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

Proof

Step	Hyp	Ref	Expression
1		cnvco	⊢ ◡ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ∘ 𝐵 ) = ( ◡ 𝐵 ∘ ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) )
2		cnvnonrel	⊢ ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅
3	2	coeq2i	⊢ ( ◡ 𝐵 ∘ ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) ) = ( ◡ 𝐵 ∘ ∅ )
4		co02	⊢ ( ◡ 𝐵 ∘ ∅ ) = ∅
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	⊢ ( ( 𝐴 ∖ ◡ ◡ 𝐴 ) ∘ 𝐵 ) = ∅