Metamath Proof Explorer


Theorem iscllaw

Description: The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020)

Ref Expression
Assertion iscllaw Could not format assertion : No typesetting found for |- ( ( .o. e. V /\ M e. W ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 simpr Could not format ( ( o = .o. /\ m = M ) -> m = M ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> m = M ) with typecode |-
2 oveq Could not format ( o = .o. -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( o = .o. -> ( x o y ) = ( x .o. y ) ) with typecode |-
3 2 adantr Could not format ( ( o = .o. /\ m = M ) -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( x o y ) = ( x .o. y ) ) with typecode |-
4 3 1 eleq12d Could not format ( ( o = .o. /\ m = M ) -> ( ( x o y ) e. m <-> ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( ( x o y ) e. m <-> ( x .o. y ) e. M ) ) with typecode |-
5 1 4 raleqbidv Could not format ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) e. m <-> A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) e. m <-> A. y e. M ( x .o. y ) e. M ) ) with typecode |-
6 1 5 raleqbidv Could not format ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) e. m <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) e. m <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) with typecode |-
7 df-cllaw clLaw = o m | x m y m x o y m
8 6 7 brabga Could not format ( ( .o. e. V /\ M e. W ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( .o. e. V /\ M e. W ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) with typecode |-