Definition df-omul

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

	Ref	Expression
Assertion	df-omul	⊢ ·o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 +o 𝑥 ) ) , ∅ ) ‘ 𝑦 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		comu	⊢ ·o
1		vx	⊢ 𝑥
2		con0	⊢ On
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5		cvv	⊢ V
6	4	cv	⊢ 𝑧
7		coa	⊢ +o
8	1	cv	⊢ 𝑥
9	6 8 7	co	⊢ ( 𝑧 +o 𝑥 )
10	4 5 9	cmpt	⊢ ( 𝑧 ∈ V ↦ ( 𝑧 +o 𝑥 ) )
11		c0	⊢ ∅
12	10 11	crdg	⊢ rec ( ( 𝑧 ∈ V ↦ ( 𝑧 +o 𝑥 ) ) , ∅ )
13	3	cv	⊢ 𝑦
14	13 12	cfv	⊢ ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 +o 𝑥 ) ) , ∅ ) ‘ 𝑦 )
15	1 3 2 2 14	cmpo	⊢ ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 +o 𝑥 ) ) , ∅ ) ‘ 𝑦 ) )
16	0 15	wceq	⊢ ·o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 +o 𝑥 ) ) , ∅ ) ‘ 𝑦 ) )