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 ${⊢}\left({A}\circ {B}\right)\circ {C}={A}\circ \left({B}\circ {C}\right)$

Proof

Step Hyp Ref Expression
1 relco ${⊢}\mathrm{Rel}\left(\left({A}\circ {B}\right)\circ {C}\right)$
2 relco ${⊢}\mathrm{Rel}\left({A}\circ \left({B}\circ {C}\right)\right)$
3 excom ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
4 anass ${⊢}\left(\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)↔\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
5 4 2exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
6 3 5 bitr4i ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)$
7 vex ${⊢}{z}\in \mathrm{V}$
8 vex ${⊢}{y}\in \mathrm{V}$
9 7 8 brco ${⊢}{z}\left({A}\circ {B}\right){y}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}{B}{w}\wedge {w}{A}{y}\right)$
10 9 anbi2i ${⊢}\left({x}{C}{z}\wedge {z}\left({A}\circ {B}\right){y}\right)↔\left({x}{C}{z}\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
11 10 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}\left({A}\circ {B}\right){y}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
12 vex ${⊢}{x}\in \mathrm{V}$
13 12 8 opelco ${⊢}⟨{x},{y}⟩\in \left(\left({A}\circ {B}\right)\circ {C}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}\left({A}\circ {B}\right){y}\right)$
14 exdistr ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
15 11 13 14 3bitr4i ${⊢}⟨{x},{y}⟩\in \left(\left({A}\circ {B}\right)\circ {C}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge \left({z}{B}{w}\wedge {w}{A}{y}\right)\right)$
16 vex ${⊢}{w}\in \mathrm{V}$
17 12 16 brco ${⊢}{x}\left({B}\circ {C}\right){w}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}{B}{w}\right)$
18 17 anbi1i ${⊢}\left({x}\left({B}\circ {C}\right){w}\wedge {w}{A}{y}\right)↔\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)$
19 18 exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\left({x}\left({B}\circ {C}\right){w}\wedge {w}{A}{y}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)$
20 12 8 opelco ${⊢}⟨{x},{y}⟩\in \left({A}\circ \left({B}\circ {C}\right)\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({x}\left({B}\circ {C}\right){w}\wedge {w}{A}{y}\right)$
21 19.41v ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)↔\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)$
22 21 exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)$
23 19 20 22 3bitr4i ${⊢}⟨{x},{y}⟩\in \left({A}\circ \left({B}\circ {C}\right)\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}{C}{z}\wedge {z}{B}{w}\right)\wedge {w}{A}{y}\right)$
24 6 15 23 3bitr4i ${⊢}⟨{x},{y}⟩\in \left(\left({A}\circ {B}\right)\circ {C}\right)↔⟨{x},{y}⟩\in \left({A}\circ \left({B}\circ {C}\right)\right)$
25 1 2 24 eqrelriiv ${⊢}\left({A}\circ {B}\right)\circ {C}={A}\circ \left({B}\circ {C}\right)$