Theorem conrel1d

Description: Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019)

	Ref	Expression
Hypothesis	conrel1d.a	$$⊢\phi \to A^{-1}=\varnothing$$
Assertion	conrel1d	$$⊢\phi \to A\circ B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		conrel1d.a	$$⊢\phi \to A^{-1}=\varnothing$$
2		incom	$$⊢\mathrm{dom}A\cap \mathrm{ran}B=\mathrm{ran}B\cap \mathrm{dom}A$$
3		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
4	1	rneqd	$$⊢\phi \to \mathrm{ran}{A}^{-1}=\mathrm{ran}\varnothing$$
5		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
6	4 5	eqtrdi	$$⊢\phi \to \mathrm{ran}{A}^{-1}=\varnothing$$
7	3 6	syl5eq	$$⊢\phi \to \mathrm{dom}A=\varnothing$$
8		ineq2	$$⊢\mathrm{dom}A=\varnothing \to \mathrm{ran}B\cap \mathrm{dom}A=\mathrm{ran}B\cap \varnothing$$
9		in0	$$⊢\mathrm{ran}B\cap \varnothing =\varnothing$$
10	8 9	eqtrdi	$$⊢\mathrm{dom}A=\varnothing \to \mathrm{ran}B\cap \mathrm{dom}A=\varnothing$$
11	7 10	syl	$$⊢\phi \to \mathrm{ran}B\cap \mathrm{dom}A=\varnothing$$
12	2 11	syl5eq	$$⊢\phi \to \mathrm{dom}A\cap \mathrm{ran}B=\varnothing$$
13	12	coemptyd	$$⊢\phi \to A\circ B=\varnothing$$