Theorem cononrel2

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

	Ref	Expression
Assertion	cononrel2	$$⊢A\circ \left(B\setminus {B^{-1}}^{-1}\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		cnvco	$$⊢{\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)}^{-1}={\left(B\setminus {B^{-1}}^{-1}\right)}^{-1}\circ A^{-1}$$
2		cnvnonrel	$$⊢{\left(B\setminus {B^{-1}}^{-1}\right)}^{-1}=\varnothing$$
3	2	coeq1i	$$⊢{\left(B\setminus {B^{-1}}^{-1}\right)}^{-1}\circ A^{-1}=\varnothing \circ A^{-1}$$
4		co01	$$⊢\varnothing \circ A^{-1}=\varnothing$$
5	1 3 4	3eqtri	$$⊢{\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)}^{-1}=\varnothing$$
6	5	cnveqi	$$⊢{{\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)}^{-1}}^{-1}={\varnothing }^{-1}$$
7		relco	$$⊢\mathrm{Rel}\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)$$
8		dfrel2	$$⊢\mathrm{Rel}\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)\leftrightarrow {{\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)}^{-1}}^{-1}=A\circ \left(B\setminus {B^{-1}}^{-1}\right)$$
9	7 8	mpbi	$$⊢{{\left(A\circ \left(B\setminus {B^{-1}}^{-1}\right)\right)}^{-1}}^{-1}=A\circ \left(B\setminus {B^{-1}}^{-1}\right)$$
10		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
11	6 9 10	3eqtr3i	$$⊢A\circ \left(B\setminus {B^{-1}}^{-1}\right)=\varnothing$$