Metamath Proof Explorer

Theorem coassOLD

Description: Obsolete version of coass as of 25-Oct-2026. (Contributed by NM, 27-Jan-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion coassOLD 
|- ( ( A o. B ) o. C ) = ( A o. ( B o. C ) )

Proof

Step Hyp Ref Expression
1 relco 
 |-  Rel ( ( A o. B ) o. C )
2 relco 
 |-  Rel ( A o. ( B o. C ) )
3 excom 
 |-  ( E. z E. w ( x C z /\ ( z B w /\ w A y ) ) <-> E. w E. z ( x C z /\ ( z B w /\ w A y ) ) )
4 anass 
 |-  ( ( ( x C z /\ z B w ) /\ w A y ) <-> ( x C z /\ ( z B w /\ w A y ) ) )
5 4 2exbii 
 |-  ( E. w E. z ( ( x C z /\ z B w ) /\ w A y ) <-> E. w E. z ( x C z /\ ( z B w /\ w A y ) ) )
6 3 5 bitr4i 
 |-  ( E. z E. w ( x C z /\ ( z B w /\ w A y ) ) <-> E. w E. z ( ( x C z /\ z B w ) /\ w A y ) )
7 vex 
 |-  z e. _V
8 vex 
 |-  y e. _V
9 7 8 brco 
 |-  ( z ( A o. B ) y <-> E. w ( z B w /\ w A y ) )
10 9 anbi2i 
 |-  ( ( x C z /\ z ( A o. B ) y ) <-> ( x C z /\ E. w ( z B w /\ w A y ) ) )
11 10 exbii 
 |-  ( E. z ( x C z /\ z ( A o. B ) y ) <-> E. z ( x C z /\ E. w ( z B w /\ w A y ) ) )
12 vex 
 |-  x e. _V
13 12 8 opelco 
 |-  ( <. x , y >. e. ( ( A o. B ) o. C ) <-> E. z ( x C z /\ z ( A o. B ) y ) )
14 exdistr 
 |-  ( E. z E. w ( x C z /\ ( z B w /\ w A y ) ) <-> E. z ( x C z /\ E. w ( z B w /\ w A y ) ) )
15 11 13 14 3bitr4i 
 |-  ( <. x , y >. e. ( ( A o. B ) o. C ) <-> E. z E. w ( x C z /\ ( z B w /\ w A y ) ) )
16 vex 
 |-  w e. _V
17 12 16 brco 
 |-  ( x ( B o. C ) w <-> E. z ( x C z /\ z B w ) )
18 17 anbi1i 
 |-  ( ( x ( B o. C ) w /\ w A y ) <-> ( E. z ( x C z /\ z B w ) /\ w A y ) )
19 18 exbii 
 |-  ( E. w ( x ( B o. C ) w /\ w A y ) <-> E. w ( E. z ( x C z /\ z B w ) /\ w A y ) )
20 12 8 opelco 
 |-  ( <. x , y >. e. ( A o. ( B o. C ) ) <-> E. w ( x ( B o. C ) w /\ w A y ) )
21 19.41v 
 |-  ( E. z ( ( x C z /\ z B w ) /\ w A y ) <-> ( E. z ( x C z /\ z B w ) /\ w A y ) )
22 21 exbii 
 |-  ( E. w E. z ( ( x C z /\ z B w ) /\ w A y ) <-> E. w ( E. z ( x C z /\ z B w ) /\ w A y ) )
23 19 20 22 3bitr4i 
 |-  ( <. x , y >. e. ( A o. ( B o. C ) ) <-> E. w E. z ( ( x C z /\ z B w ) /\ w A y ) )
24 6 15 23 3bitr4i 
 |-  ( <. x , y >. e. ( ( A o. B ) o. C ) <-> <. x , y >. e. ( A o. ( B o. C ) ) )
25 1 2 24 eqrelriiv 
 |-  ( ( A o. B ) o. C ) = ( A o. ( B o. C ) )