Theorem co02

Description: Composition with the empty set. Theorem 20 of Suppes p. 63. (Contributed by NM, 24-Apr-2004)

	Ref	Expression
Assertion	co02	$$⊢A\circ \varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		relco	$$⊢\mathrm{Rel}\left(A\circ \varnothing \right)$$
2		rel0	$$⊢\mathrm{Rel}\varnothing$$
3		br0	$$⊢\neg x\varnothing z$$
4	3	intnanr	$$⊢\neg \left(x\varnothing z\wedge zAy\right)$$
5	4	nex	$$⊢\neg \exists z\left(x\varnothing z\wedge zAy\right)$$
6		vex	$$⊢x\in \mathrm{V}$$
7		vex	$$⊢y\in \mathrm{V}$$
8	6 7	opelco	$$⊢⟨x,y⟩\in \left(A\circ \varnothing \right)\leftrightarrow \exists z\left(x\varnothing z\wedge zAy\right)$$
9	5 8	mtbir	$$⊢\neg ⟨x,y⟩\in \left(A\circ \varnothing \right)$$
10		noel	$$⊢\neg ⟨x,y⟩\in \varnothing$$
11	9 10	2false	$$⊢⟨x,y⟩\in \left(A\circ \varnothing \right)\leftrightarrow ⟨x,y⟩\in \varnothing$$
12	1 2 11	eqrelriiv	$$⊢A\circ \varnothing =\varnothing$$