Metamath Proof Explorer

Theorem coass

Description: Associative law for class composition. Theorem 27 of Suppes p. 64. Also Exercise 21 of Enderton p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997)

Ref Expression
Assertion coass ⊢A∘B∘C=A∘B∘C

Proof

Step Hyp Ref Expression
1 relco ⊢Rel⁡A∘B∘C
2 relco ⊢Rel⁡A∘B∘C
3 excom ⊢∃z∃wxCz∧zBw∧wAy↔∃w∃zxCz∧zBw∧wAy
4 anass ⊢xCz∧zBw∧wAy↔xCz∧zBw∧wAy
5 4 2exbii ⊢∃w∃zxCz∧zBw∧wAy↔∃w∃zxCz∧zBw∧wAy
6 3 5 bitr4i ⊢∃z∃wxCz∧zBw∧wAy↔∃w∃zxCz∧zBw∧wAy
7 vex ⊢z∈V
8 vex ⊢y∈V
9 7 8 brco ⊢zA∘By↔∃wzBw∧wAy
10 9 anbi2i ⊢xCz∧zA∘By↔xCz∧∃wzBw∧wAy
11 10 exbii ⊢∃zxCz∧zA∘By↔∃zxCz∧∃wzBw∧wAy
12 vex ⊢x∈V
13 12 8 opelco ⊢xy∈A∘B∘C↔∃zxCz∧zA∘By
14 exdistr ⊢∃z∃wxCz∧zBw∧wAy↔∃zxCz∧∃wzBw∧wAy
15 11 13 14 3bitr4i ⊢xy∈A∘B∘C↔∃z∃wxCz∧zBw∧wAy
16 vex ⊢w∈V
17 12 16 brco ⊢xB∘Cw↔∃zxCz∧zBw
18 17 anbi1i ⊢xB∘Cw∧wAy↔∃zxCz∧zBw∧wAy
19 18 exbii ⊢∃wxB∘Cw∧wAy↔∃w∃zxCz∧zBw∧wAy
20 12 8 opelco ⊢xy∈A∘B∘C↔∃wxB∘Cw∧wAy
21 19.41v ⊢∃zxCz∧zBw∧wAy↔∃zxCz∧zBw∧wAy
22 21 exbii ⊢∃w∃zxCz∧zBw∧wAy↔∃w∃zxCz∧zBw∧wAy
23 19 20 22 3bitr4i ⊢xy∈A∘B∘C↔∃w∃zxCz∧zBw∧wAy
24 6 15 23 3bitr4i ⊢xy∈A∘B∘C↔xy∈A∘B∘C
25 1 2 24 eqrelriiv ⊢A∘B∘C=A∘B∘C