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) Remove dependency on ax-11 . (Revised by BJ, 25-Oct-2026)

		Ref	Expression
	Assertion	coass	$⊢ (A \circ B) \circ C = A \circ (B \circ C)$

Proof

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel ((A \circ B) \circ C)$
2		relco	$⊢ Rel (A \circ (B \circ C))$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	brco	$⊢ x ((A \circ B) \circ C) y \leftrightarrow \exists z (x C z \land z (A \circ B) y)$
6		vex	$⊢ z \in V$
7	6 4	brco	$⊢ z (A \circ B) y \leftrightarrow \exists w (z B w \land w A y)$
8		vex	$⊢ w \in V$
9	3 6 8	brcoi	$⊢ (x C z \land z B w) \to x (B \circ C) w$
10	3 8 4	brcoi	$⊢ (x (B \circ C) w \land w A y) \to x (A \circ (B \circ C)) y$
11	9 10	sylan	$⊢ ((x C z \land z B w) \land w A y) \to x (A \circ (B \circ C)) y$
12	11	anasss	$⊢ (x C z \land (z B w \land w A y)) \to x (A \circ (B \circ C)) y$
13	12	ex	$⊢ x C z \to ((z B w \land w A y) \to x (A \circ (B \circ C)) y)$
14	13	exlimdv	$⊢ x C z \to (\exists w (z B w \land w A y) \to x (A \circ (B \circ C)) y)$
15	7 14	biimtrid	$⊢ x C z \to (z (A \circ B) y \to x (A \circ (B \circ C)) y)$
16	15	imp	$⊢ (x C z \land z (A \circ B) y) \to x (A \circ (B \circ C)) y$
17	16	exlimiv	$⊢ \exists z (x C z \land z (A \circ B) y) \to x (A \circ (B \circ C)) y$
18	5 17	sylbi	$⊢ x ((A \circ B) \circ C) y \to x (A \circ (B \circ C)) y$
19	3 4	brco	$⊢ x (A \circ (B \circ C)) y \leftrightarrow \exists w (x (B \circ C) w \land w A y)$
20	3 8	brco	$⊢ x (B \circ C) w \leftrightarrow \exists z (x C z \land z B w)$
21	6 8 4	brcoi	$⊢ (z B w \land w A y) \to z (A \circ B) y$
22	3 6 4	brcoi	$⊢ (x C z \land z (A \circ B) y) \to x ((A \circ B) \circ C) y$
23	21 22	sylan2	$⊢ (x C z \land (z B w \land w A y)) \to x ((A \circ B) \circ C) y$
24	23	anassrs	$⊢ ((x C z \land z B w) \land w A y) \to x ((A \circ B) \circ C) y$
25	24	ex	$⊢ (x C z \land z B w) \to (w A y \to x ((A \circ B) \circ C) y)$
26	25	exlimiv	$⊢ \exists z (x C z \land z B w) \to (w A y \to x ((A \circ B) \circ C) y)$
27	20 26	sylbi	$⊢ x (B \circ C) w \to (w A y \to x ((A \circ B) \circ C) y)$
28	27	imp	$⊢ (x (B \circ C) w \land w A y) \to x ((A \circ B) \circ C) y$
29	28	exlimiv	$⊢ \exists w (x (B \circ C) w \land w A y) \to x ((A \circ B) \circ C) y$
30	19 29	sylbi	$⊢ x (A \circ (B \circ C)) y \to x ((A \circ B) \circ C) y$
31	18 30	impbii	$⊢ x ((A \circ B) \circ C) y \leftrightarrow x (A \circ (B \circ C)) y$
32	1 2 31	eqbrriv	$⊢ (A \circ B) \circ C = A \circ (B \circ C)$

Metamath Proof Explorer

Theorem coass

Proof