Theorem iscomlaw

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

	Ref	Expression
Assertion	iscomlaw	Could not format assertion : No typesetting found for |- ( ( .o. e. V /\ M e. W ) -> ( .o. comLaw M <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) ) 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		oveq	Could not format ( o = .o. -> ( y o x ) = ( y .o. x ) ) : No typesetting found for |- ( o = .o. -> ( y o x ) = ( y .o. x ) ) with typecode |-
4	2 3	eqeq12d	Could not format ( o = .o. -> ( ( x o y ) = ( y o x ) <-> ( x .o. y ) = ( y .o. x ) ) ) : No typesetting found for |- ( o = .o. -> ( ( x o y ) = ( y o x ) <-> ( x .o. y ) = ( y .o. x ) ) ) with typecode |-
5	4	adantr	Could not format ( ( o = .o. /\ m = M ) -> ( ( x o y ) = ( y o x ) <-> ( x .o. y ) = ( y .o. x ) ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( ( x o y ) = ( y o x ) <-> ( x .o. y ) = ( y .o. x ) ) ) with typecode |-
6	1 5	raleqbidv	Could not format ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) = ( y o x ) <-> A. y e. M ( x .o. y ) = ( y .o. x ) ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) = ( y o x ) <-> A. y e. M ( x .o. y ) = ( y .o. x ) ) ) with typecode |-
7	1 6	raleqbidv	Could not format ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) = ( y o x ) <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) = ( y o x ) <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) ) with typecode |-
8		df-comlaw	$$⊢\mathrm{comLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in mxoy=yox\right\}$$
9	7 8	brabga	Could not format ( ( .o. e. V /\ M e. W ) -> ( .o. comLaw M <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) ) : No typesetting found for |- ( ( .o. e. V /\ M e. W ) -> ( .o. comLaw M <-> A. x e. M A. y e. M ( x .o. y ) = ( y .o. x ) ) ) with typecode |-