Theorem intop

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

	Ref	Expression
Assertion	intop	⊢ ( ⚬ ∈ ( 𝑀 intOp 𝑁 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		df-intop	⊢ intOp = ( 𝑚 ∈ V , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) )
2	1	elmpocl	⊢ ( ⚬ ∈ ( 𝑀 intOp 𝑁 ) → ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) )
3		intopval	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) → ( 𝑀 intOp 𝑁 ) = ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) )
4	3	eleq2d	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) → ( ⚬ ∈ ( 𝑀 intOp 𝑁 ) ↔ ⚬ ∈ ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) ) )
5		elmapi	⊢ ( ⚬ ∈ ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑁 )
6	4 5	biimtrdi	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) → ( ⚬ ∈ ( 𝑀 intOp 𝑁 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑁 ) )
7	2 6	mpcom	⊢ ( ⚬ ∈ ( 𝑀 intOp 𝑁 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑁 )