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

Metamath Proof Explorer

Theorem oav

Description: Value of ordinal addition. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oav ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rdgeq2 ⊢ ( 𝑦 = 𝐴 → rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝑦 ) = rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) )
2 1 fveq1d ⊢ ( 𝑦 = 𝐴 → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝑦 ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
3 fveq2 ⊢ ( 𝑧 = 𝐵 → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
4 df-oadd ⊢ +o = ( 𝑦 ∈ On , 𝑧 ∈ On ↦ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝑦 ) ‘ 𝑧 ) )
5 fvex ⊢ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ∈ V
6 2 3 4 5 ovmpo ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )