Metamath Proof Explorer

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 ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ ↔ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 incom ⊢ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 )
2 cocnvcnv1 ⊢ ( ◡ ◡ 𝐴 ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 )
3 2 ineq2i ⊢ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) = ( 𝐶 ∩ ( 𝐴 ∘ 𝐵 ) )
4 incom ⊢ ( 𝐶 ∩ ( 𝐴 ∘ 𝐵 ) ) = ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 )
5 3 4 eqtri ⊢ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) = ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 )
6 id ⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ → ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ )
7 5 6 eqtrid ⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ → ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) = ∅ )
8 coeq2 ⊢ ( ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) = ∅ → ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) ) = ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ∅ ) )
9 co02 ⊢ ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ∅ ) = ∅
10 8 9 eqtrdi ⊢ ( ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) = ∅ → ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) ) = ∅ )
11 comodular ⊢ ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 ) ⊆ ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) )
12 sseq0 ⊢ ( ( ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 ) ⊆ ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) ) ∧ ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) ) = ∅ ) → ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 ) = ∅ )
13 11 12 mpan ⊢ ( ( ( ◡ 𝐴 ∩ ( 𝐵 ∘ ◡ 𝐶 ) ) ∘ ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) ) = ∅ → ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 ) = ∅ )
14 10 13 syl ⊢ ( ( 𝐶 ∩ ( ◡ ◡ 𝐴 ∘ 𝐵 ) ) = ∅ → ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 ) = ∅ )
15 7 14 syl ⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ → ( ( ◡ 𝐴 ∘ 𝐶 ) ∩ 𝐵 ) = ∅ )
16 1 15 eqtrid ⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ → ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ∅ )
17 coeq2 ⊢ ( ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ∅ → ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) = ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ∅ ) )
18 co02 ⊢ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ∅ ) = ∅
19 17 18 eqtrdi ⊢ ( ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ∅ → ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) = ∅ )
20 comodular ⊢ ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) ⊆ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) )
21 sseq0 ⊢ ( ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) ⊆ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) ∧ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) = ∅ ) → ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ )
22 20 21 mpan ⊢ ( ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) = ∅ → ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ )
23 19 22 syl ⊢ ( ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ∅ → ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ )
24 16 23 impbii ⊢ ( ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) = ∅ ↔ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) = ∅ )