Theorem conrel1d

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

	Ref	Expression
Hypothesis	conrel1d.a	|- ( ph -> `' A = (/) )
Assertion	conrel1d	|- ( ph -> ( A o. B ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		conrel1d.a	|- ( ph -> `' A = (/) )
2		incom	|- ( dom A i^i ran B ) = ( ran B i^i dom A )
3		dfdm4	|- dom A = ran `' A
4	1	rneqd	|- ( ph -> ran `' A = ran (/) )
5		rn0	|- ran (/) = (/)
6	4 5	eqtrdi	|- ( ph -> ran `' A = (/) )
7	3 6	syl5eq	|- ( ph -> dom A = (/) )
8		ineq2	|- ( dom A = (/) -> ( ran B i^i dom A ) = ( ran B i^i (/) ) )
9		in0	|- ( ran B i^i (/) ) = (/)
10	8 9	eqtrdi	|- ( dom A = (/) -> ( ran B i^i dom A ) = (/) )
11	7 10	syl	|- ( ph -> ( ran B i^i dom A ) = (/) )
12	2 11	syl5eq	|- ( ph -> ( dom A i^i ran B ) = (/) )
13	12	coemptyd	|- ( ph -> ( A o. B ) = (/) )