Theorem recnauxfst ≪ | index | src | ≫ 

theorem recnauxfst (S: set) (n z: nat): $ fst (recnaux z S n) = n $;
StepHypRefExpression
1 eqidd 
_1 = n -> z = z
2 eqsidd 
_1 = n -> S == S
3 id 
_1 = n -> _1 = n
4 1, 2, 3 recnauxeqd 
_1 = n -> recnaux z S _1 = recnaux z S n
5 4 fsteqd 
_1 = n -> fst (recnaux z S _1) = fst (recnaux z S n)
6 5, 3 eqeqd 
_1 = n -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S n) = n)
7 eqidd 
_1 = 0 -> z = z
8 eqsidd 
_1 = 0 -> S == S
9 id 
_1 = 0 -> _1 = 0
10 7, 8, 9 recnauxeqd 
_1 = 0 -> recnaux z S _1 = recnaux z S 0
11 10 fsteqd 
_1 = 0 -> fst (recnaux z S _1) = fst (recnaux z S 0)
12 11, 9 eqeqd 
_1 = 0 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S 0) = 0)
13 eqidd 
_1 = a1 -> z = z
14 eqsidd 
_1 = a1 -> S == S
15 id 
_1 = a1 -> _1 = a1
16 13, 14, 15 recnauxeqd 
_1 = a1 -> recnaux z S _1 = recnaux z S a1
17 16 fsteqd 
_1 = a1 -> fst (recnaux z S _1) = fst (recnaux z S a1)
18 17, 15 eqeqd 
_1 = a1 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S a1) = a1)
19 eqidd 
_1 = suc a1 -> z = z
20 eqsidd 
_1 = suc a1 -> S == S
21 id 
_1 = suc a1 -> _1 = suc a1
22 19, 20, 21 recnauxeqd 
_1 = suc a1 -> recnaux z S _1 = recnaux z S (suc a1)
23 22 fsteqd 
_1 = suc a1 -> fst (recnaux z S _1) = fst (recnaux z S (suc a1))
24 23, 21 eqeqd 
_1 = suc a1 -> (fst (recnaux z S _1) = _1 <-> fst (recnaux z S (suc a1)) = suc a1)
25 eqtr 
fst (recnaux z S 0) = fst (0, z) -> fst (0, z) = 0 -> fst (recnaux z S 0) = 0
26 fsteq 
recnaux z S 0 = 0, z -> fst (recnaux z S 0) = fst (0, z)
27 recnaux0 
recnaux z S 0 = 0, z
28 26, 27 ax_mp 
fst (recnaux z S 0) = fst (0, z)
29 25, 28 ax_mp 
fst (0, z) = 0 -> fst (recnaux z S 0) = 0
30 fstpr 
fst (0, z) = 0
31 29, 30 ax_mp 
fst (recnaux z S 0) = 0
32 eqtr 
fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) ->
  fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1)) ->
  fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
33 fsteq 
recnaux z S (suc a1) = suc (fst (recnaux z S a1)), S @ recnaux z S a1 -> fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1)
34 recnauxS2 
recnaux z S (suc a1) = suc (fst (recnaux z S a1)), S @ recnaux z S a1
35 33, 34 ax_mp 
fst (recnaux z S (suc a1)) = fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1)
36 32, 35 ax_mp 
fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1)) -> fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
37 fstpr 
fst (suc (fst (recnaux z S a1)), S @ recnaux z S a1) = suc (fst (recnaux z S a1))
38 36, 37 ax_mp 
fst (recnaux z S (suc a1)) = suc (fst (recnaux z S a1))
39 suceq 
fst (recnaux z S a1) = a1 -> suc (fst (recnaux z S a1)) = suc a1
40 38, 39 syl5eq 
fst (recnaux z S a1) = a1 -> fst (recnaux z S (suc a1)) = suc a1
41 6, 12, 18, 24, 31, 40 ind 
fst (recnaux z S n) = 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)