Metamath Proof Explorer

Theorem assintopass

Description: An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

Ref Expression
Assertion assintopass 
|- ( .o. e. ( assIntOp ` M ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( .o. e. ( assIntOp ` M ) -> .o. e. ( assIntOp ` M ) )
2 elfvex 
 |-  ( .o. e. ( assIntOp ` M ) -> M e. _V )
3 assintopasslaw 
 |-  ( .o. e. ( assIntOp ` M ) -> .o. assLaw M )
4 isasslaw 
 |-  ( ( .o. e. ( assIntOp ` M ) /\ 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 ) ) ) )
5 3 4 syl5ibcom 
 |-  ( .o. e. ( assIntOp ` M ) -> ( ( .o. e. ( assIntOp ` M ) /\ M e. _V ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
6 1 2 5 mp2and 
 |-  ( .o. e. ( assIntOp ` M ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )