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	$⊢ (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		excom	$⊢ \exists z \exists w (x C z \land (z B w \land w A y)) \leftrightarrow \exists w \exists z (x C z \land (z B w \land w A y))$
4		anass	$⊢ ((x C z \land z B w) \land w A y) \leftrightarrow (x C z \land (z B w \land w A y))$
5	4	2exbii	$⊢ \exists w \exists z ((x C z \land z B w) \land w A y) \leftrightarrow \exists w \exists z (x C z \land (z B w \land w A y))$
6	3 5	bitr4i	$⊢ \exists z \exists w (x C z \land (z B w \land w A y)) \leftrightarrow \exists w \exists z ((x C z \land z B w) \land w A y)$
7		vex	$⊢ z \in V$
8		vex	$⊢ y \in V$
9	7 8	brco	$⊢ z (A \circ B) y \leftrightarrow \exists w (z B w \land w A y)$
10	9	anbi2i	$⊢ (x C z \land z (A \circ B) y) \leftrightarrow (x C z \land \exists w (z B w \land w A y))$
11	10	exbii	$⊢ \exists z (x C z \land z (A \circ B) y) \leftrightarrow \exists z (x C z \land \exists w (z B w \land w A y))$
12		vex	$⊢ x \in V$
13	12 8	opelco	$⊢ ⟨x, y⟩ \in ((A \circ B) \circ C) \leftrightarrow \exists z (x C z \land z (A \circ B) y)$
14		exdistr	$⊢ \exists z \exists w (x C z \land (z B w \land w A y)) \leftrightarrow \exists z (x C z \land \exists w (z B w \land w A y))$
15	11 13 14	3bitr4i	$⊢ ⟨x, y⟩ \in ((A \circ B) \circ C) \leftrightarrow \exists z \exists w (x C z \land (z B w \land w A y))$
16		vex	$⊢ w \in V$
17	12 16	brco	$⊢ x (B \circ C) w \leftrightarrow \exists z (x C z \land z B w)$
18	17	anbi1i	$⊢ (x (B \circ C) w \land w A y) \leftrightarrow (\exists z (x C z \land z B w) \land w A y)$
19	18	exbii	$⊢ \exists w (x (B \circ C) w \land w A y) \leftrightarrow \exists w (\exists z (x C z \land z B w) \land w A y)$
20	12 8	opelco	$⊢ ⟨x, y⟩ \in (A \circ (B \circ C)) \leftrightarrow \exists w (x (B \circ C) w \land w A y)$
21		19.41v	$⊢ \exists z ((x C z \land z B w) \land w A y) \leftrightarrow (\exists z (x C z \land z B w) \land w A y)$
22	21	exbii	$⊢ \exists w \exists z ((x C z \land z B w) \land w A y) \leftrightarrow \exists w (\exists z (x C z \land z B w) \land w A y)$
23	19 20 22	3bitr4i	$⊢ ⟨x, y⟩ \in (A \circ (B \circ C)) \leftrightarrow \exists w \exists z ((x C z \land z B w) \land w A y)$
24	6 15 23	3bitr4i	$⊢ ⟨x, y⟩ \in ((A \circ B) \circ C) \leftrightarrow ⟨x, y⟩ \in (A \circ (B \circ C))$
25	1 2 24	eqrelriiv	$⊢ (A \circ B) \circ C = A \circ (B \circ C)$

Metamath Proof Explorer

Theorem coassOLD

Proof