# Metamath Proof Explorer

## 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)↔{{\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$