Theorem obindS2 ≪ | index | src | ≫ 

theorem obindS2 (n: nat) {x: nat}: $ obind n (\ x, suc x) = n $;
StepHypRefExpression
1 obind0 
obind 0 (\ x, suc x) = 0
2 obindeq1 
n = 0 -> obind n (\ x, suc x) = obind 0 (\ x, suc x)
3 id 
n = 0 -> n = 0
4 2, 3 eqeqd 
n = 0 -> (obind n (\ x, suc x) = n <-> obind 0 (\ x, suc x) = 0)
5 1, 4 mpbiri 
n = 0 -> obind n (\ x, suc x) = n
6 exsuc 
n != 0 <-> E. a1 n = suc a1
7 6 conv ne 
~n = 0 <-> E. a1 n = suc a1
8 eqtr 
obind (suc a1) (\ x, suc x) = (\ x, suc x) @ a1 -> (\ x, suc x) @ a1 = suc a1 -> obind (suc a1) (\ x, suc x) = suc a1
9 obindS 
obind (suc a1) (\ x, suc x) = (\ x, suc x) @ a1
10 8, 9 ax_mp 
(\ x, suc x) @ a1 = suc a1 -> obind (suc a1) (\ x, suc x) = suc a1
11 suceq 
x = a1 -> suc x = suc a1
12 11 applame 
(\ x, suc x) @ a1 = suc a1
13 10, 12 ax_mp 
obind (suc a1) (\ x, suc x) = suc a1
14 obindeq1 
n = suc a1 -> obind n (\ x, suc x) = obind (suc a1) (\ x, suc x)
15 id 
n = suc a1 -> n = suc a1
16 14, 15 eqeqd 
n = suc a1 -> (obind n (\ x, suc x) = n <-> obind (suc a1) (\ x, suc x) = suc a1)
17 13, 16 mpbiri 
n = suc a1 -> obind n (\ x, suc x) = n
18 17 eex 
E. a1 n = suc a1 -> obind n (\ x, suc x) = n
19 7, 18 sylbi 
~n = 0 -> obind n (\ x, suc x) = n
20 5, 19 cases 
obind n (\ x, suc x) = n

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)