Metamath Proof Explorer

Theorem coassOLD

Description: Obsolete version of coass as of 25-Oct-2026. (Contributed by NM, 27-Jan-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion coassOLD ( ( 𝐴 ∘ 𝐵 ) ∘ 𝐶 ) = ( 𝐴 ∘ ( 𝐵 ∘ 𝐶 ) )

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