# Metamath Proof Explorer

## Theorem co01

Description: Composition with the empty set. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion co01 ${⊢}\varnothing \circ {A}=\varnothing$

### Proof

Step Hyp Ref Expression
1 cnv0 ${⊢}{\varnothing }^{-1}=\varnothing$
2 cnvco ${⊢}{\left(\varnothing \circ {A}\right)}^{-1}={{A}}^{-1}\circ {\varnothing }^{-1}$
3 1 coeq2i ${⊢}{{A}}^{-1}\circ {\varnothing }^{-1}={{A}}^{-1}\circ \varnothing$
4 co02 ${⊢}{{A}}^{-1}\circ \varnothing =\varnothing$
5 2 3 4 3eqtri ${⊢}{\left(\varnothing \circ {A}\right)}^{-1}=\varnothing$
6 1 5 eqtr4i ${⊢}{\varnothing }^{-1}={\left(\varnothing \circ {A}\right)}^{-1}$
7 6 cnveqi ${⊢}{{\varnothing }^{-1}}^{-1}={{\left(\varnothing \circ {A}\right)}^{-1}}^{-1}$
8 rel0 ${⊢}\mathrm{Rel}\varnothing$
9 dfrel2 ${⊢}\mathrm{Rel}\varnothing ↔{{\varnothing }^{-1}}^{-1}=\varnothing$
10 8 9 mpbi ${⊢}{{\varnothing }^{-1}}^{-1}=\varnothing$
11 relco ${⊢}\mathrm{Rel}\left(\varnothing \circ {A}\right)$
12 dfrel2 ${⊢}\mathrm{Rel}\left(\varnothing \circ {A}\right)↔{{\left(\varnothing \circ {A}\right)}^{-1}}^{-1}=\varnothing \circ {A}$
13 11 12 mpbi ${⊢}{{\left(\varnothing \circ {A}\right)}^{-1}}^{-1}=\varnothing \circ {A}$
14 7 10 13 3eqtr3ri ${⊢}\varnothing \circ {A}=\varnothing$