Theorem conrel2d

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

	Ref	Expression
Hypothesis	conrel1d.a	⊢ ( 𝜑 → ◡ 𝐴 = ∅ )
Assertion	conrel2d	⊢ ( 𝜑 → ( 𝐵 ∘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		conrel1d.a	⊢ ( 𝜑 → ◡ 𝐴 = ∅ )
2		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
3	2	ineq2i	⊢ ( dom 𝐵 ∩ ran 𝐴 ) = ( dom 𝐵 ∩ dom ◡ 𝐴 )
4	3	a1i	⊢ ( 𝜑 → ( dom 𝐵 ∩ ran 𝐴 ) = ( dom 𝐵 ∩ dom ◡ 𝐴 ) )
5	1	dmeqd	⊢ ( 𝜑 → dom ◡ 𝐴 = dom ∅ )
6	5	ineq2d	⊢ ( 𝜑 → ( dom 𝐵 ∩ dom ◡ 𝐴 ) = ( dom 𝐵 ∩ dom ∅ ) )
7		dm0	⊢ dom ∅ = ∅
8	7	ineq2i	⊢ ( dom 𝐵 ∩ dom ∅ ) = ( dom 𝐵 ∩ ∅ )
9		in0	⊢ ( dom 𝐵 ∩ ∅ ) = ∅
10	8 9	eqtri	⊢ ( dom 𝐵 ∩ dom ∅ ) = ∅
11	10	a1i	⊢ ( 𝜑 → ( dom 𝐵 ∩ dom ∅ ) = ∅ )
12	4 6 11	3eqtrd	⊢ ( 𝜑 → ( dom 𝐵 ∩ ran 𝐴 ) = ∅ )
13	12	coemptyd	⊢ ( 𝜑 → ( 𝐵 ∘ 𝐴 ) = ∅ )