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