# 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 Could not format assertion : No typesetting found for |- ( .o. e. ( assIntOp  M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) with typecode |-

### Proof

Step Hyp Ref Expression
1 elfvex Could not format ( .o. e. ( assIntOp  M ) -> M e. _V ) : No typesetting found for |- ( .o. e. ( assIntOp  M ) -> M e. _V ) with typecode |-
2 assintopmap ${⊢}{M}\in \mathrm{V}\to \mathrm{assIntOp}\left({M}\right)=\left\{{o}\in \left({{M}}^{\left({M}×{M}\right)}\right)|{o}\mathrm{assLaw}{M}\right\}$
3 2 eleq2d Could not format ( M e. _V -> ( .o. e. ( assIntOp  M ) <-> .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( assIntOp  M ) <-> .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } ) ) with typecode |-
4 breq1 Could not format ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) ) : No typesetting found for |- ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) ) with typecode |-
5 4 elrab Could not format ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } <-> ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) : No typesetting found for |- ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } <-> ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) with typecode |-
6 elmapi Could not format ( .o. e. ( M ^m ( M X. M ) ) -> .o. : ( M X. M ) --> M ) : No typesetting found for |- ( .o. e. ( M ^m ( M X. M ) ) -> .o. : ( M X. M ) --> M ) with typecode |-
7 6 anim1i Could not format ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) : No typesetting found for |- ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) with typecode |-
8 5 7 sylbi Could not format ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) : No typesetting found for |- ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) with typecode |-
9 3 8 syl6bi Could not format ( M e. _V -> ( .o. e. ( assIntOp  M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( assIntOp  M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) ) with typecode |-
10 1 9 mpcom Could not format ( .o. e. ( assIntOp  M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) ) with typecode |-