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

Metamath Proof Explorer

Theorem onasuc

Description: Addition with successor. Theorem 4I(A2) of Enderton p. 79. (Note that this version of oasuc does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 frsuc ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )
3 peano2 ⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω )
4 3 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → suc 𝐵 ∈ ω )
5 4 fvresd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) )
6 fvres ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
8 7 fveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
9 2 5 8 3eqtr3d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
10 nnon ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
11 onsuc ⊢ ( 𝐵 ∈ On → suc 𝐵 ∈ On )
12 10 11 syl ⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ On )
13 oav ⊢ ( ( 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ( 𝐴 +o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) )
14 12 13 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 +o suc 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ suc 𝐵 ) )
15 ovex ⊢ ( 𝐴 +o 𝐵 ) ∈ V
16 suceq ⊢ ( 𝑥 = ( 𝐴 +o 𝐵 ) → suc 𝑥 = suc ( 𝐴 +o 𝐵 ) )
17 eqid ⊢ ( 𝑥 ∈ V ↦ suc 𝑥 ) = ( 𝑥 ∈ V ↦ suc 𝑥 )
18 15 sucex ⊢ suc ( 𝐴 +o 𝐵 ) ∈ V
19 16 17 18 fvmpt ⊢ ( ( 𝐴 +o 𝐵 ) ∈ V → ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( 𝐴 +o 𝐵 ) ) = suc ( 𝐴 +o 𝐵 ) )
20 15 19 ax-mp ⊢ ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( 𝐴 +o 𝐵 ) ) = suc ( 𝐴 +o 𝐵 )
21 oav ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
22 10 21 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
23 22 fveq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( 𝐴 +o 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
24 20 23 eqtr3id ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → suc ( 𝐴 +o 𝐵 ) = ( ( 𝑥 ∈ V ↦ suc 𝑥 ) ‘ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ) )
25 9 14 24 3eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ ω ) → ( 𝐴 +o suc 𝐵 ) = suc ( 𝐴 +o 𝐵 ) )