Theorem conrel1d

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

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

Proof

Step	Hyp	Ref	Expression
1		conrel1d.a	⊢ ( 𝜑 → ◡ 𝐴 = ∅ )
2		incom	⊢ ( dom 𝐴 ∩ ran 𝐵 ) = ( ran 𝐵 ∩ dom 𝐴 )
3		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
4	1	rneqd	⊢ ( 𝜑 → ran ◡ 𝐴 = ran ∅ )
5		rn0	⊢ ran ∅ = ∅
6	4 5	eqtrdi	⊢ ( 𝜑 → ran ◡ 𝐴 = ∅ )
7	3 6	syl5eq	⊢ ( 𝜑 → dom 𝐴 = ∅ )
8		ineq2	⊢ ( dom 𝐴 = ∅ → ( ran 𝐵 ∩ dom 𝐴 ) = ( ran 𝐵 ∩ ∅ ) )
9		in0	⊢ ( ran 𝐵 ∩ ∅ ) = ∅
10	8 9	eqtrdi	⊢ ( dom 𝐴 = ∅ → ( ran 𝐵 ∩ dom 𝐴 ) = ∅ )
11	7 10	syl	⊢ ( 𝜑 → ( ran 𝐵 ∩ dom 𝐴 ) = ∅ )
12	2 11	syl5eq	⊢ ( 𝜑 → ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
13	12	coemptyd	⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) = ∅ )