Theorem oasuc

Description: Addition with successor. Definition 8.1 of TakeutiZaring p. 56. Definition 2.3 of Schloeder p. 4. (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		onsuc	⊢ ( 𝐵 ∈ 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 𝐵 ) )