Theorem comodular

Description: A strong modular law for the composition of relations. The modular law is an axiom defining allegories. (Contributed by BJ, 7-Nov-2026)

	Ref	Expression
Assertion	comodular	⊢ ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) ⊆ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( 𝐴 ∘ 𝐵 )
2		relin1	⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → Rel ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) )
3	1 2	ax-mp	⊢ Rel ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 )
4		brin	⊢ ( 𝑥 ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) 𝑦 ↔ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ∧ 𝑥 𝐶 𝑦 ) )
5		vex	⊢ 𝑥 ∈ V
6		vex	⊢ 𝑦 ∈ V
7	5 6	brco	⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
8		simprl	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑥 𝐵 𝑧 )
9		simpl	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑥 𝐶 𝑦 )
10		simprr	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑧 𝐴 𝑦 )
11		vex	⊢ 𝑧 ∈ V
12	6 11	brcnv	⊢ ( 𝑦 ◡ 𝐴 𝑧 ↔ 𝑧 𝐴 𝑦 )
13	10 12	sylibr	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑦 ◡ 𝐴 𝑧 )
14	5 6 11	brcoi	⊢ ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 ◡ 𝐴 𝑧 ) → 𝑥 ( ◡ 𝐴 ∘ 𝐶 ) 𝑧 )
15	9 13 14	syl2anc	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑥 ( ◡ 𝐴 ∘ 𝐶 ) 𝑧 )
16		brin	⊢ ( 𝑥 ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) 𝑧 ↔ ( 𝑥 𝐵 𝑧 ∧ 𝑥 ( ◡ 𝐴 ∘ 𝐶 ) 𝑧 ) )
17	8 15 16	sylanbrc	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑥 ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) 𝑧 )
18	11 5	brcnv	⊢ ( 𝑧 ◡ 𝐵 𝑥 ↔ 𝑥 𝐵 𝑧 )
19	8 18	sylibr	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑧 ◡ 𝐵 𝑥 )
20	11 5 6	brcoi	⊢ ( ( 𝑧 ◡ 𝐵 𝑥 ∧ 𝑥 𝐶 𝑦 ) → 𝑧 ( 𝐶 ∘ ◡ 𝐵 ) 𝑦 )
21	19 9 20	syl2anc	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑧 ( 𝐶 ∘ ◡ 𝐵 ) 𝑦 )
22		brin	⊢ ( 𝑧 ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) 𝑦 ↔ ( 𝑧 𝐴 𝑦 ∧ 𝑧 ( 𝐶 ∘ ◡ 𝐵 ) 𝑦 ) )
23	10 21 22	sylanbrc	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑧 ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) 𝑦 )
24	5 11 6	brcoi	⊢ ( ( 𝑥 ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) 𝑧 ∧ 𝑧 ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) 𝑦 ) → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 )
25	17 23 24	syl2anc	⊢ ( ( 𝑥 𝐶 𝑦 ∧ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 )
26	25	ex	⊢ ( 𝑥 𝐶 𝑦 → ( ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 ) )
27	26	exlimdv	⊢ ( 𝑥 𝐶 𝑦 → ( ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 ) )
28	7 27	biimtrid	⊢ ( 𝑥 𝐶 𝑦 → ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 ) )
29	28	impcom	⊢ ( ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑦 ∧ 𝑥 𝐶 𝑦 ) → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 )
30	4 29	sylbi	⊢ ( 𝑥 ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) 𝑦 → 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 )
31		df-br	⊢ ( 𝑥 ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) )
32		df-br	⊢ ( 𝑥 ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) )
33	30 31 32	3imtr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) ) )
34	3 33	relssi	⊢ ( ( 𝐴 ∘ 𝐵 ) ∩ 𝐶 ) ⊆ ( ( 𝐴 ∩ ( 𝐶 ∘ ◡ 𝐵 ) ) ∘ ( 𝐵 ∩ ( ◡ 𝐴 ∘ 𝐶 ) ) )