Theorem coass 4782

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.)

Assertion

Ref	Expression
coass	⊢ ((A ∘ B) ∘ 𝐶) = (A ∘ (B ∘ 𝐶))

Proof of Theorem coass

Dummy variables x y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 4762	. 2 ⊢ Rel ((A ∘ B) ∘ 𝐶)
2		relco 4762	. 2 ⊢ Rel (A ∘ (B ∘ 𝐶))
3		excom 1551	. . . 4 ⊢ (∃z∃w(x𝐶z ∧ (zBw ∧ wAy)) ↔ ∃w∃z(x𝐶z ∧ (zBw ∧ wAy)))
4		anass 381	. . . . 5 ⊢ (((x𝐶z ∧ zBw) ∧ wAy) ↔ (x𝐶z ∧ (zBw ∧ wAy)))
5	4	2exbii 1494	. . . 4 ⊢ (∃w∃z((x𝐶z ∧ zBw) ∧ wAy) ↔ ∃w∃z(x𝐶z ∧ (zBw ∧ wAy)))
6	3, 5	bitr4i 176	. . 3 ⊢ (∃z∃w(x𝐶z ∧ (zBw ∧ wAy)) ↔ ∃w∃z((x𝐶z ∧ zBw) ∧ wAy))
7		vex 2554	. . . . . . 7 ⊢ z ∈ V
8		vex 2554	. . . . . . 7 ⊢ y ∈ V
9	7, 8	brco 4449	. . . . . 6 ⊢ (z(A ∘ B)y ↔ ∃w(zBw ∧ wAy))
10	9	anbi2i 430	. . . . 5 ⊢ ((x𝐶z ∧ z(A ∘ B)y) ↔ (x𝐶z ∧ ∃w(zBw ∧ wAy)))
11	10	exbii 1493	. . . 4 ⊢ (∃z(x𝐶z ∧ z(A ∘ B)y) ↔ ∃z(x𝐶z ∧ ∃w(zBw ∧ wAy)))
12		vex 2554	. . . . 5 ⊢ x ∈ V
13	12, 8	opelco 4450	. . . 4 ⊢ (⟨x, y⟩ ∈ ((A ∘ B) ∘ 𝐶) ↔ ∃z(x𝐶z ∧ z(A ∘ B)y))
14		exdistr 1784	. . . 4 ⊢ (∃z∃w(x𝐶z ∧ (zBw ∧ wAy)) ↔ ∃z(x𝐶z ∧ ∃w(zBw ∧ wAy)))
15	11, 13, 14	3bitr4i 201	. . 3 ⊢ (⟨x, y⟩ ∈ ((A ∘ B) ∘ 𝐶) ↔ ∃z∃w(x𝐶z ∧ (zBw ∧ wAy)))
16		vex 2554	. . . . . . 7 ⊢ w ∈ V
17	12, 16	brco 4449	. . . . . 6 ⊢ (x(B ∘ 𝐶)w ↔ ∃z(x𝐶z ∧ zBw))
18	17	anbi1i 431	. . . . 5 ⊢ ((x(B ∘ 𝐶)w ∧ wAy) ↔ (∃z(x𝐶z ∧ zBw) ∧ wAy))
19	18	exbii 1493	. . . 4 ⊢ (∃w(x(B ∘ 𝐶)w ∧ wAy) ↔ ∃w(∃z(x𝐶z ∧ zBw) ∧ wAy))
20	12, 8	opelco 4450	. . . 4 ⊢ (⟨x, y⟩ ∈ (A ∘ (B ∘ 𝐶)) ↔ ∃w(x(B ∘ 𝐶)w ∧ wAy))
21		19.41v 1779	. . . . 5 ⊢ (∃z((x𝐶z ∧ zBw) ∧ wAy) ↔ (∃z(x𝐶z ∧ zBw) ∧ wAy))
22	21	exbii 1493	. . . 4 ⊢ (∃w∃z((x𝐶z ∧ zBw) ∧ wAy) ↔ ∃w(∃z(x𝐶z ∧ zBw) ∧ wAy))
23	19, 20, 22	3bitr4i 201	. . 3 ⊢ (⟨x, y⟩ ∈ (A ∘ (B ∘ 𝐶)) ↔ ∃w∃z((x𝐶z ∧ zBw) ∧ wAy))
24	6, 15, 23	3bitr4i 201	. 2 ⊢ (⟨x, y⟩ ∈ ((A ∘ B) ∘ 𝐶) ↔ ⟨x, y⟩ ∈ (A ∘ (B ∘ 𝐶)))
25	1, 2, 24	eqrelriiv 4377	1 ⊢ ((A ∘ B) ∘ 𝐶) = (A ∘ (B ∘ 𝐶))

Syntax hints:   ∧ wa 97   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755   ∘ ccom 4292

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-co 4297

This theorem is referenced by:  funcoeqres  5100  fcof1o  5372  tposco  5831