Theorem isassintop

Description: The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

	Ref	Expression
Assertion	isassintop	Could not format assertion : No typesetting found for |- ( M e. V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. : ( M X. M ) --> 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		assintopmap	$$⊢M\in V\to \mathrm{assIntOp}\left(M\right)=\left\{o\in \left(M^{\left(M\times M\right)}\right)|o\mathrm{assLaw}M\right\}$$
2	1	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 |-
3		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 |-
4	3	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 |-
5	2 4	syl6bb	Could not format ( M e. V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) ) : No typesetting found for |- ( M e. V -> ( .o. e. ( assIntOp ` 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	ad2antrl	Could not format ( ( M e. V /\ ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) -> .o. : ( M X. M ) --> M ) : No typesetting found for |- ( ( M e. V /\ ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) -> .o. : ( M X. M ) --> M ) with typecode |-
8		isasslaw	Could not format ( ( .o. e. ( M ^m ( M X. 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 ) ) ) ) : No typesetting found for |- ( ( .o. e. ( M ^m ( M X. 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 ) ) ) ) with typecode |-
9	8	biimpd	Could not format ( ( .o. e. ( M ^m ( M X. 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 ) ) ) ) : No typesetting found for |- ( ( .o. e. ( M ^m ( M X. 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 ) ) ) ) with typecode |-
10	9	impancom	Could not format ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw 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 ) ) ) ) : No typesetting found for |- ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw 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 ) ) ) ) with typecode |-
11	10	impcom	Could not format ( ( M e. V /\ ( .o. e. ( M ^m ( M X. 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 |- ( ( M e. V /\ ( .o. e. ( M ^m ( M X. 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 |-
12	7 11	jca	Could not format ( ( M e. V /\ ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) -> ( .o. : ( M X. M ) --> 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 |- ( ( M e. V /\ ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) -> ( .o. : ( M X. M ) --> 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 |-
13	12	ex	Could not format ( M e. V -> ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) -> ( .o. : ( M X. M ) --> 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 |- ( M e. V -> ( ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) -> ( .o. : ( M X. M ) --> 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 |-
14	5 13	sylbid	Could not format ( M e. V -> ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> 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 |- ( M e. V -> ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> 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 |-
15		isclintop	Could not format ( M e. V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) ) : No typesetting found for |- ( M e. V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) ) with typecode |-
16	15	biimprcd	Could not format ( .o. : ( M X. M ) --> M -> ( M e. V -> .o. e. ( clIntOp ` M ) ) ) : No typesetting found for |- ( .o. : ( M X. M ) --> M -> ( M e. V -> .o. e. ( clIntOp ` M ) ) ) with typecode |-
17	16	adantr	Could not format ( ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) -> ( M e. V -> .o. e. ( clIntOp ` M ) ) ) : No typesetting found for |- ( ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) -> ( M e. V -> .o. e. ( clIntOp ` M ) ) ) with typecode |-
18	17	impcom	Could not format ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> .o. e. ( clIntOp ` M ) ) : No typesetting found for |- ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> .o. e. ( clIntOp ` M ) ) with typecode |-
19		sqxpexg	$$⊢M\in V\to M\times M\in \mathrm{V}$$
20		fex	Could not format ( ( .o. : ( M X. M ) --> M /\ ( M X. M ) e. _V ) -> .o. e. _V ) : No typesetting found for |- ( ( .o. : ( M X. M ) --> M /\ ( M X. M ) e. _V ) -> .o. e. _V ) with typecode |-
21	19 20	sylan2	Could not format ( ( .o. : ( M X. M ) --> M /\ M e. V ) -> .o. e. _V ) : No typesetting found for |- ( ( .o. : ( M X. M ) --> M /\ M e. V ) -> .o. e. _V ) with typecode |-
22	21	ancoms	Could not format ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> .o. e. _V ) : No typesetting found for |- ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> .o. e. _V ) with typecode |-
23		simpl	Could not format ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> M e. V ) : No typesetting found for |- ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> M e. V ) with typecode |-
24		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 |-
25	24	bicomd	Could not format ( ( .o. e. _V /\ 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 ) ) <-> .o. assLaw M ) ) : No typesetting found for |- ( ( .o. e. _V /\ 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 ) ) <-> .o. assLaw M ) ) with typecode |-
26	22 23 25	syl2anc	Could not format ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> ( A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> .o. assLaw M ) ) : No typesetting found for |- ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> ( A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> .o. assLaw M ) ) with typecode |-
27	26	biimpd	Could not format ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> ( A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) -> .o. assLaw M ) ) : No typesetting found for |- ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> ( A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) -> .o. assLaw M ) ) with typecode |-
28	27	impr	Could not format ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> .o. assLaw M ) : No typesetting found for |- ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> .o. assLaw M ) with typecode |-
29		assintopval	$$⊢M\in V\to \mathrm{assIntOp}\left(M\right)=\left\{o\in \mathrm{clIntOp}\left(M\right)|o\mathrm{assLaw}M\right\}$$
30	29	adantr	Could not format ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } ) : No typesetting found for |- ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } ) with typecode |-
31	30	eleq2d	Could not format ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( clIntOp ` M ) | o assLaw M } ) ) : No typesetting found for |- ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( clIntOp ` M ) | o assLaw M } ) ) with typecode |-
32	3	elrab	Could not format ( .o. e. { o e. ( clIntOp ` M ) | o assLaw M } <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) : No typesetting found for |- ( .o. e. { o e. ( clIntOp ` M ) | o assLaw M } <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) with typecode |-
33	31 32	syl6bb	Could not format ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> ( .o. e. ( assIntOp ` M ) <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) ) : No typesetting found for |- ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> ( .o. e. ( assIntOp ` M ) <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) ) ) with typecode |-
34	18 28 33	mpbir2and	Could not format ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> .o. e. ( assIntOp ` M ) ) : No typesetting found for |- ( ( M e. V /\ ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) -> .o. e. ( assIntOp ` M ) ) with typecode |-
35	34	ex	Could not format ( M e. V -> ( ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) -> .o. e. ( assIntOp ` M ) ) ) : No typesetting found for |- ( M e. V -> ( ( .o. : ( M X. M ) --> M /\ A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) -> .o. e. ( assIntOp ` M ) ) ) with typecode |-
36	14 35	impbid	Could not format ( M e. V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. : ( M X. M ) --> 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 |- ( M e. V -> ( .o. e. ( assIntOp ` M ) <-> ( .o. : ( M X. M ) --> 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 |-