Metamath Proof Explorer

Theorem clcllaw

Description: Closure of a closed operation. (Contributed by FL, 14-Sep-2010) (Revised by AV, 21-Jan-2020)

Ref Expression
Assertion clcllaw 
|- ( ( .o. clLaw M /\ X e. M /\ Y e. M ) -> ( X .o. Y ) e. M )

Proof

Step Hyp Ref Expression
1 df-cllaw 
 |-  clLaw = { <. o , m >. | A. x e. m A. y e. m ( x o y ) e. m }
2 1 bropaex12 
 |-  ( .o. clLaw M -> ( .o. e. _V /\ M e. _V ) )
3 iscllaw 
 |-  ( ( .o. e. _V /\ M e. _V ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) )
4 ovrspc2v 
 |-  ( ( ( X e. M /\ Y e. M ) /\ A. x e. M A. y e. M ( x .o. y ) e. M ) -> ( X .o. Y ) e. M )
5 4 expcom 
 |-  ( A. x e. M A. y e. M ( x .o. y ) e. M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) )
6 3 5 biimtrdi 
 |-  ( ( .o. e. _V /\ M e. _V ) -> ( .o. clLaw M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) ) )
7 2 6 mpcom 
 |-  ( .o. clLaw M -> ( ( X e. M /\ Y e. M ) -> ( X .o. Y ) e. M ) )
8 7 3impib 
 |-  ( ( .o. clLaw M /\ X e. M /\ Y e. M ) -> ( X .o. Y ) e. M )