Theorem asslawass

Description: Associativity of an associative operation. (Contributed by FL, 2-Nov-2009) (Revised by AV, 21-Jan-2020)

	Ref	Expression
Assertion	asslawass	Could not format assertion : No typesetting found for |- ( .o. assLaw M -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-asslaw	$$⊢\mathrm{assLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in m\forall z\in m\left(xoy\right)oz=xo\left(yoz\right)\right\}$$
2	1	bropaex12	Could not format ( .o. assLaw M -> ( .o. e. _V /\ M e. _V ) ) : No typesetting found for |- ( .o. assLaw M -> ( .o. e. _V /\ M e. _V ) ) with typecode |-
3		isasslaw	Could not format ( ( .o. e. _V /\ M e. _V ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( .o. e. _V /\ M e. _V ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
4	2 3	syl	Could not format ( .o. assLaw M -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( .o. assLaw M -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
5	4	ibi	Could not format ( .o. assLaw M -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( .o. assLaw M -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-