Metamath Proof Explorer


Theorem oasuc

Description: Addition with successor. Definition 8.1 of TakeutiZaring p. 56. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion oasuc ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o suc 𝐵 ) = suc ( 𝐴 +o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rdgsuc ( 𝐵 ∈ On → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
2 1 adantl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
3 suceloni ( 𝐵 ∈ On → suc 𝐵 ∈ On )
4 oav ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ( 𝐴 +o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) )
5 3 4 sylan2 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) )
6 ovex ( 𝐴 +o 𝐵 ) ∈ V
7 suceq ( 𝑥 = ( 𝐴 +o 𝐵 ) → suc 𝑥 = suc ( 𝐴 +o 𝐵 ) )
8 eqid ( 𝑥 ∈ V ↦ suc 𝑥 ) = ( 𝑥 ∈ V ↦ suc 𝑥 )
9 6 sucex suc ( 𝐴 +o 𝐵 ) ∈ V
10 7 8 9 fvmpt ( ( 𝐴 +o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( 𝐴 +o 𝐵 ) ) = suc ( 𝐴 +o 𝐵 ) )
11 6 10 ax-mp ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( 𝐴 +o 𝐵 ) ) = suc ( 𝐴 +o 𝐵 )
12 oav ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
13 12 fveq2d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
14 11 13 eqtr3id ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ( 𝐴 +o 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
15 2 5 14 3eqtr4d ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o suc 𝐵 ) = suc ( 𝐴 +o 𝐵 ) )