Theorem intopval

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

	Ref	Expression
Assertion	intopval	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝑀 intOp 𝑁 ) = ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-intop	⊢ intOp = ( 𝑚 ∈ V , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) )
2	1	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → intOp = ( 𝑚 ∈ V , 𝑛 ∈ V ↦ ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) ) )
3		simpr	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → 𝑛 = 𝑁 )
4		simpl	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → 𝑚 = 𝑀 )
5	4	sqxpeqd	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → ( 𝑚 × 𝑚 ) = ( 𝑀 × 𝑀 ) )
6	3 5	oveq12d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) = ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) )
7	6	adantl	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) ) → ( 𝑛 ↑m ( 𝑚 × 𝑚 ) ) = ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) )
8		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
9	8	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝑀 ∈ V )
10		elex	⊢ ( 𝑁 ∈ 𝑊 → 𝑁 ∈ V )
11	10	adantl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → 𝑁 ∈ V )
12		ovexd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) ∈ V )
13	2 7 9 11 12	ovmpod	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝑀 intOp 𝑁 ) = ( 𝑁 ↑m ( 𝑀 × 𝑀 ) ) )