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\times 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 |-