Metamath Proof Explorer

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 
|- ( 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 assintopmap 
 |-  ( M e. V -> ( assIntOp ` M ) = { o e. ( M ^m ( M X. M ) ) | o assLaw M } )
2 1 eleq2d 
 |-  ( M e. V -> ( .o. e. ( assIntOp ` M ) <-> .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } ) )
3 breq1 
 |-  ( o = .o. -> ( o assLaw M <-> .o. assLaw M ) )
4 3 elrab 
 |-  ( .o. e. { o e. ( M ^m ( M X. M ) ) | o assLaw M } <-> ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) )
5 2 4 bitrdi 
 |-  ( M e. V -> ( .o. e. ( assIntOp ` 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 ad2antrl 
 |-  ( ( M e. V /\ ( .o. e. ( M ^m ( M X. M ) ) /\ .o. assLaw M ) ) -> .o. : ( M X. M ) --> M )
8 isasslaw 
 |-  ( ( .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 ) ) ) )
9 8 biimpd 
 |-  ( ( .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 ) ) ) )
10 9 impancom 
 |-  ( ( .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 ) ) ) )
11 10 impcom 
 |-  ( ( 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 ) ) )
12 7 11 jca 
 |-  ( ( 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 ) ) ) )
13 12 ex 
 |-  ( 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 ) ) ) ) )
14 5 13 sylbid 
 |-  ( 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 ) ) ) ) )
15 isclintop 
 |-  ( M e. V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) )
16 15 biimprcd 
 |-  ( .o. : ( M X. M ) --> M -> ( M e. V -> .o. e. ( clIntOp ` M ) ) )
17 16 adantr 
 |-  ( ( .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 ) ) )
18 17 impcom 
 |-  ( ( 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 ) )
19 sqxpexg 
 |-  ( M e. V -> ( M X. M ) e. _V )
20 fex 
 |-  ( ( .o. : ( M X. M ) --> M /\ ( M X. M ) e. _V ) -> .o. e. _V )
21 19 20 sylan2 
 |-  ( ( .o. : ( M X. M ) --> M /\ M e. V ) -> .o. e. _V )
22 21 ancoms 
 |-  ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> .o. e. _V )
23 simpl 
 |-  ( ( M e. V /\ .o. : ( M X. M ) --> M ) -> M e. V )
24 isasslaw 
 |-  ( ( .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 ) ) ) )
25 24 bicomd 
 |-  ( ( .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 ) )
26 22 23 25 syl2anc 
 |-  ( ( 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 ) )
27 26 biimpd 
 |-  ( ( 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 ) )
28 27 impr 
 |-  ( ( 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 )
29 assintopval 
 |-  ( M e. V -> ( assIntOp ` M ) = { o e. ( clIntOp ` M ) | o assLaw M } )
30 29 adantr 
 |-  ( ( 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 } )
31 30 eleq2d 
 |-  ( ( 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 } ) )
32 3 elrab 
 |-  ( .o. e. { o e. ( clIntOp ` M ) | o assLaw M } <-> ( .o. e. ( clIntOp ` M ) /\ .o. assLaw M ) )
33 31 32 bitrdi 
 |-  ( ( 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 ) ) )
34 18 28 33 mpbir2and 
 |-  ( ( 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 ) )
35 34 ex 
 |-  ( 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 ) ) )
36 14 35 impbid 
 |-  ( 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 ) ) ) ) )