Theorem coineq0

Description: A composition ( A o. B ) is disjoint from a class C if and only if B is disjoint from (`' A o. C ) ` . This is a form of the Schroeder rule that does not use complements. See also coeq0 . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coineq0	|- ( ( ( A o. B ) i^i C ) = (/) <-> ( B i^i ( `' A o. C ) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		incom	|- ( B i^i ( `' A o. C ) ) = ( ( `' A o. C ) i^i B )
2		cocnvcnv1	|- ( `' `' A o. B ) = ( A o. B )
3	2	ineq2i	|- ( C i^i ( `' `' A o. B ) ) = ( C i^i ( A o. B ) )
4		incom	|- ( C i^i ( A o. B ) ) = ( ( A o. B ) i^i C )
5	3 4	eqtri	|- ( C i^i ( `' `' A o. B ) ) = ( ( A o. B ) i^i C )
6		id	|- ( ( ( A o. B ) i^i C ) = (/) -> ( ( A o. B ) i^i C ) = (/) )
7	5 6	eqtrid	|- ( ( ( A o. B ) i^i C ) = (/) -> ( C i^i ( `' `' A o. B ) ) = (/) )
8		coeq2	|- ( ( C i^i ( `' `' A o. B ) ) = (/) -> ( ( `' A i^i ( B o. `' C ) ) o. ( C i^i ( `' `' A o. B ) ) ) = ( ( `' A i^i ( B o. `' C ) ) o. (/) ) )
9		co02	|- ( ( `' A i^i ( B o. `' C ) ) o. (/) ) = (/)
10	8 9	eqtrdi	|- ( ( C i^i ( `' `' A o. B ) ) = (/) -> ( ( `' A i^i ( B o. `' C ) ) o. ( C i^i ( `' `' A o. B ) ) ) = (/) )
11		comodular	|- ( ( `' A o. C ) i^i B ) C_ ( ( `' A i^i ( B o. `' C ) ) o. ( C i^i ( `' `' A o. B ) ) )
12		sseq0	|- ( ( ( ( `' A o. C ) i^i B ) C_ ( ( `' A i^i ( B o. `' C ) ) o. ( C i^i ( `' `' A o. B ) ) ) /\ ( ( `' A i^i ( B o. `' C ) ) o. ( C i^i ( `' `' A o. B ) ) ) = (/) ) -> ( ( `' A o. C ) i^i B ) = (/) )
13	11 12	mpan	|- ( ( ( `' A i^i ( B o. `' C ) ) o. ( C i^i ( `' `' A o. B ) ) ) = (/) -> ( ( `' A o. C ) i^i B ) = (/) )
14	10 13	syl	|- ( ( C i^i ( `' `' A o. B ) ) = (/) -> ( ( `' A o. C ) i^i B ) = (/) )
15	7 14	syl	|- ( ( ( A o. B ) i^i C ) = (/) -> ( ( `' A o. C ) i^i B ) = (/) )
16	1 15	eqtrid	|- ( ( ( A o. B ) i^i C ) = (/) -> ( B i^i ( `' A o. C ) ) = (/) )
17		coeq2	|- ( ( B i^i ( `' A o. C ) ) = (/) -> ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) = ( ( A i^i ( C o. `' B ) ) o. (/) ) )
18		co02	|- ( ( A i^i ( C o. `' B ) ) o. (/) ) = (/)
19	17 18	eqtrdi	|- ( ( B i^i ( `' A o. C ) ) = (/) -> ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) = (/) )
20		comodular	|- ( ( A o. B ) i^i C ) C_ ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) )
21		sseq0	|- ( ( ( ( A o. B ) i^i C ) C_ ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) /\ ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) = (/) ) -> ( ( A o. B ) i^i C ) = (/) )
22	20 21	mpan	|- ( ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) = (/) -> ( ( A o. B ) i^i C ) = (/) )
23	19 22	syl	|- ( ( B i^i ( `' A o. C ) ) = (/) -> ( ( A o. B ) i^i C ) = (/) )
24	16 23	impbii	|- ( ( ( A o. B ) i^i C ) = (/) <-> ( B i^i ( `' A o. C ) ) = (/) )