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	$$⊢\mathrm{clLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in mxoy\in m\right\}$$
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 |-