# Metamath Proof Explorer

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