Metamath Proof Explorer

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 
|- ( ( A o. B ) i^i C ) C_ ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( A o. B )
2 relin1 
 |-  ( Rel ( A o. B ) -> Rel ( ( A o. B ) i^i C ) )
3 1 2 ax-mp 
 |-  Rel ( ( A o. B ) i^i C )
4 brin 
 |-  ( x ( ( A o. B ) i^i C ) y <-> ( x ( A o. B ) y /\ x C y ) )
5 vex 
 |-  x e. _V
6 vex 
 |-  y e. _V
7 5 6 brco 
 |-  ( x ( A o. B ) y <-> E. z ( x B z /\ z A y ) )
8 simprl 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> x B z )
9 simpl 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> x C y )
10 simprr 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> z A y )
11 vex 
 |-  z e. _V
12 6 11 brcnv 
 |-  ( y `' A z <-> z A y )
13 10 12 sylibr 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> y `' A z )
14 5 6 11 brcoi 
 |-  ( ( x C y /\ y `' A z ) -> x ( `' A o. C ) z )
15 9 13 14 syl2anc 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> x ( `' A o. C ) z )
16 brin 
 |-  ( x ( B i^i ( `' A o. C ) ) z <-> ( x B z /\ x ( `' A o. C ) z ) )
17 8 15 16 sylanbrc 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> x ( B i^i ( `' A o. C ) ) z )
18 11 5 brcnv 
 |-  ( z `' B x <-> x B z )
19 8 18 sylibr 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> z `' B x )
20 11 5 6 brcoi 
 |-  ( ( z `' B x /\ x C y ) -> z ( C o. `' B ) y )
21 19 9 20 syl2anc 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> z ( C o. `' B ) y )
22 brin 
 |-  ( z ( A i^i ( C o. `' B ) ) y <-> ( z A y /\ z ( C o. `' B ) y ) )
23 10 21 22 sylanbrc 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> z ( A i^i ( C o. `' B ) ) y )
24 5 11 6 brcoi 
 |-  ( ( x ( B i^i ( `' A o. C ) ) z /\ z ( A i^i ( C o. `' B ) ) y ) -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y )
25 17 23 24 syl2anc 
 |-  ( ( x C y /\ ( x B z /\ z A y ) ) -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y )
26 25 ex 
 |-  ( x C y -> ( ( x B z /\ z A y ) -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y ) )
27 26 exlimdv 
 |-  ( x C y -> ( E. z ( x B z /\ z A y ) -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y ) )
28 7 27 biimtrid 
 |-  ( x C y -> ( x ( A o. B ) y -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y ) )
29 28 impcom 
 |-  ( ( x ( A o. B ) y /\ x C y ) -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y )
30 4 29 sylbi 
 |-  ( x ( ( A o. B ) i^i C ) y -> x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y )
31 df-br 
 |-  ( x ( ( A o. B ) i^i C ) y <-> <. x , y >. e. ( ( A o. B ) i^i C ) )
32 df-br 
 |-  ( x ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) y <-> <. x , y >. e. ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) )
33 30 31 32 3imtr3i 
 |-  ( <. x , y >. e. ( ( A o. B ) i^i C ) -> <. x , y >. e. ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) ) )
34 3 33 relssi 
 |-  ( ( A o. B ) i^i C ) C_ ( ( A i^i ( C o. `' B ) ) o. ( B i^i ( `' A o. C ) ) )