Theorem cononrel1

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

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

Proof

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