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	Could not format assertion : No typesetting found for |- ( .o. e. ( clIntOp ` M ) -> .o. clLaw M ) with typecode |-

Proof

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