This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) = ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 )
2 relco ⊢ Rel ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) )
3 excom ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
4 anass ⊢ ( ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) ↔ ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
5 4 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑧 ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
6 3 5 bitr4i ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) )
7 vex ⊢ 𝑧 ∈ V
8 vex ⊢ 𝑦 ∈ V
9 7 8 brco ⊢ ( 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑦 ↔ ∃ 𝑤 ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) )
10 9 anbi2i ⊢ ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑦 ) ↔ ( 𝑥 𝐶 𝑧 ∧ ∃ 𝑤 ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
11 10 exbii ⊢ ( ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑦 ) ↔ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ ∃ 𝑤 ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
12 vex ⊢ 𝑥 ∈ V
13 12 8 opelco ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) ↔ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 ( 𝐴 ∘ 𝐵 ) 𝑦 ) )
14 exdistr ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ ∃ 𝑤 ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
15 11 13 14 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑥 𝐶 𝑧 ∧ ( 𝑧 𝐵 𝑤 ∧ 𝑤 𝐴 𝑦 ) ) )
16 vex ⊢ 𝑤 ∈ V
17 12 16 brco ⊢ ( 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑤 ↔ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) )
18 17 anbi1i ⊢ ( ( 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑤 ∧ 𝑤 𝐴 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) )
19 18 exbii ⊢ ( ∃ 𝑤 ( 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑤 ∧ 𝑤 𝐴 𝑦 ) ↔ ∃ 𝑤 ( ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) )
20 12 8 opelco ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) ↔ ∃ 𝑤 ( 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑤 ∧ 𝑤 𝐴 𝑦 ) )
21 19.41v ⊢ ( ∃ 𝑧 ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) )
22 21 exbii ⊢ ( ∃ 𝑤 ∃ 𝑧 ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) ↔ ∃ 𝑤 ( ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) )
23 19 20 22 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ( ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑤 ) ∧ 𝑤 𝐴 𝑦 ) )
24 6 15 23 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) ) )
25 1 2 24 eqrelriiv ⊢ ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) = ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) )