This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) ) , ∅ ) ‘ 𝐵 ) )