Theorem omv

Description: Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	omv	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 +o 𝑦 ) = ( 𝑥 +o 𝐴 ) )
2	1	mpteq2dv	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝑦 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) )
3		rdgeq1	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝑦 ) ) = ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) → rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝑦 ) ) , ∅ ) = rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) )
4	2 3	syl	⊢ ( 𝑦 = 𝐴 → rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝑦 ) ) , ∅ ) = rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) )
5	4	fveq1d	⊢ ( 𝑦 = 𝐴 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝑦 ) ) , ∅ ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝑧 ) )
6		fveq2	⊢ ( 𝑧 = 𝐵 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )
7		df-omul	⊢ ·o = ( 𝑦 ∈ On , 𝑧 ∈ On ↦ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝑦 ) ) , ∅ ) ‘ 𝑧 ) )
8		fvex	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) ∈ V
9	5 6 7 8	ovmpo	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )