Metamath Proof Explorer

Theorem intopval

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

Ref Expression
Assertion intopval ⊢ M ∈ V ∧ N ∈ W → M intOp N = N M × M

Proof

Step Hyp Ref Expression
1 df-intop ⊢ intOp = m ∈ V , n ∈ V ⟼ n m × m
2 1 a1i ⊢ M ∈ V ∧ N ∈ W → intOp = m ∈ V , n ∈ V ⟼ n m × m
3 simpr ⊢ m = M ∧ n = N → n = N
4 simpl ⊢ m = M ∧ n = N → m = M
5 4 sqxpeqd ⊢ m = M ∧ n = N → m × m = M × M
6 3 5 oveq12d ⊢ m = M ∧ n = N → n m × m = N M × M
7 6 adantl ⊢ M ∈ V ∧ N ∈ W ∧ m = M ∧ n = N → n m × m = N M × M
8 elex ⊢ M ∈ V → M ∈ V
9 8 adantr ⊢ M ∈ V ∧ N ∈ W → M ∈ V
10 elex ⊢ N ∈ W → N ∈ V
11 10 adantl ⊢ M ∈ V ∧ N ∈ W → N ∈ V
12 ovexd ⊢ M ∈ V ∧ N ∈ W → N M × M ∈ V
13 2 7 9 11 12 ovmpod ⊢ M ∈ V ∧ N ∈ W → M intOp N = N M × M