Metamath Proof Explorer

Definition df-omul

Description: Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995)

Ref Expression
Assertion df-omul ⊢ ⋅ 𝑜 = x ∈ On , y ∈ On ⟼ rec ⁡ z ∈ V ⟼ z + 𝑜 x ∅ ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 comu class ⋅ 𝑜
1 vx setvar x
2 con0 class On
3 vy setvar y
4 vz setvar z
5 cvv class V
6 4 cv setvar z
7 coa class + 𝑜
8 1 cv setvar x
9 6 8 7 co class z + 𝑜 x
10 4 5 9 cmpt class z ∈ V ⟼ z + 𝑜 x
11 c0 class ∅
12 10 11 crdg class rec ⁡ z ∈ V ⟼ z + 𝑜 x ∅
13 3 cv setvar y
14 13 12 cfv class rec ⁡ z ∈ V ⟼ z + 𝑜 x ∅ ⁡ y
15 1 3 2 2 14 cmpo class x ∈ On , y ∈ On ⟼ rec ⁡ z ∈ V ⟼ z + 𝑜 x ∅ ⁡ y
16 0 15 wceq wff ⋅ 𝑜 = x ∈ On , y ∈ On ⟼ rec ⁡ z ∈ V ⟼ z + 𝑜 x ∅ ⁡ y