Metamath Proof Explorer

Theorem assintop

Description: An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion assintop 
|- ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( .o. e. ( assIntOp ` M ) -> M e. _V )
2 assintopmap 
 |-  ( M e. _V -> ( assIntOp ` M ) = { o e. ( M ^m ( M X. M ) ) | o assLaw M } )
3 2 eleq2d 
 |-  ( M e. _V -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } ) )
4 breq1 
 |-  ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) )
5 4 elrab 
 |-  ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } <-> ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) )
6 elmapi 
 |-  ( .o. e. ( M ^m ( M X. M ) ) -> .o. : ( M X. M ) --> M )
7 6 anim1i 
 |-  ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) )
8 5 7 sylbi 
 |-  ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) )
9 3 8 syl6bi 
 |-  ( M e. _V -> ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) )
10 1 9 mpcom 
 |-  ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) )