Metamath Proof Explorer

Theorem clintopcllaw

Description: The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion clintopcllaw 
|- ( .o. e. ( clIntOp ` M ) -> .o. clLaw M )

Proof

Step Hyp Ref Expression
1 clintop 
 |-  ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M )
2 ffnov 
 |-  ( .o. : ( M X. M ) --> M <-> ( .o. Fn ( M X. M ) /\ A. x e. M A. y e. M ( x .o. y ) e. M ) )
3 2 simprbi 
 |-  ( .o. : ( M X. M ) --> M -> A. x e. M A. y e. M ( x .o. y ) e. M )
4 1 3 syl 
 |-  ( .o. e. ( clIntOp ` M ) -> A. x e. M A. y e. M ( x .o. y ) e. M )
5 elfvex 
 |-  ( .o. e. ( clIntOp ` M ) -> M e. _V )
6 iscllaw 
 |-  ( ( .o. e. ( clIntOp ` M ) /\ M e. _V ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) )
7 5 6 mpdan 
 |-  ( .o. e. ( clIntOp ` M ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) )
8 4 7 mpbird 
 |-  ( .o. e. ( clIntOp ` M ) -> .o. clLaw M )