Theorem clintop

Description: A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	clintop	Could not format assertion : No typesetting found for |- ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elfvex	Could not format ( .o. e. ( clIntOp ` M ) -> M e. _V ) : No typesetting found for |- ( .o. e. ( clIntOp ` M ) -> M e. _V ) with typecode |-
2		isclintop	Could not format ( M e. _V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( clIntOp ` M ) <-> .o. : ( M X. M ) --> M ) ) with typecode |-
3	2	biimpd	Could not format ( M e. _V -> ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M ) ) : No typesetting found for |- ( M e. _V -> ( .o. e. ( clIntOp ` M ) -> .o. : ( M X. M ) --> M ) ) with typecode |-
4	1 3	mpcom	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 |-