Theorem intop

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

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

Proof

Step	Hyp	Ref	Expression
1		df-intop	$$⊢\mathrm{intOp}=\left(m\in \mathrm{V},n\in \mathrm{V}⟼n^{\left(m\times m\right)}\right)$$
2	1	elmpocl	Could not format ( .o. e. ( M intOp N ) -> ( M e. _V /\ N e. _V ) ) : No typesetting found for |- ( .o. e. ( M intOp N ) -> ( M e. _V /\ N e. _V ) ) with typecode |-
3		intopval	$$⊢\left(M\in \mathrm{V}\wedge N\in \mathrm{V}\right)\to M\mathrm{intOp}N=N^{\left(M\times M\right)}$$
4	3	eleq2d	Could not format ( ( M e. _V /\ N e. _V ) -> ( .o. e. ( M intOp N ) <-> .o. e. ( N ^m ( M X. M ) ) ) ) : No typesetting found for |- ( ( M e. _V /\ N e. _V ) -> ( .o. e. ( M intOp N ) <-> .o. e. ( N ^m ( M X. M ) ) ) ) with typecode |-
5		elmapi	Could not format ( .o. e. ( N ^m ( M X. M ) ) -> .o. : ( M X. M ) --> N ) : No typesetting found for |- ( .o. e. ( N ^m ( M X. M ) ) -> .o. : ( M X. M ) --> N ) with typecode |-
6	4 5	syl6bi	Could not format ( ( M e. _V /\ N e. _V ) -> ( .o. e. ( M intOp N ) -> .o. : ( M X. M ) --> N ) ) : No typesetting found for |- ( ( M e. _V /\ N e. _V ) -> ( .o. e. ( M intOp N ) -> .o. : ( M X. M ) --> N ) ) with typecode |-
7	2 6	mpcom	Could not format ( .o. e. ( M intOp N ) -> .o. : ( M X. M ) --> N ) : No typesetting found for |- ( .o. e. ( M intOp N ) -> .o. : ( M X. M ) --> N ) with typecode |-