Theorem ocaseS ≪ | index | src | ≫ 

theorem ocaseS (S: set) (n z: nat): $ ocase z S @ suc n = S @ n $;
StepHypRefExpression
1 eqtr 
ocase z S @ suc n = recn z (\ i, S @ fst i) (suc n) -> recn z (\ i, S @ fst i) (suc n) = S @ n -> ocase z S @ suc n = S @ n
2 ocaseval 
ocase z S @ suc n = recn z (\ i, S @ fst i) (suc n)
3 1, 2 ax_mp 
recn z (\ i, S @ fst i) (suc n) = S @ n -> ocase z S @ suc n = S @ n
4 eqtr 
recn z (\ i, S @ fst i) (suc n) = (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) ->
  (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) = S @ n ->
  recn z (\ i, S @ fst i) (suc n) = S @ n
5 recnS 
recn z (\ i, S @ fst i) (suc n) = (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n)
6 4, 5 ax_mp 
(\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) = S @ n -> recn z (\ i, S @ fst i) (suc n) = S @ n
7 eqtr3 
(\ i, S @ fst i) @ (n, ocase z S @ n) = (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) ->
  (\ i, S @ fst i) @ (n, ocase z S @ n) = S @ n ->
  (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) = S @ n
8 appeq2 
n, ocase z S @ n = n, recn z (\ i, S @ fst i) n -> (\ i, S @ fst i) @ (n, ocase z S @ n) = (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n)
9 preq2 
ocase z S @ n = recn z (\ i, S @ fst i) n -> n, ocase z S @ n = n, recn z (\ i, S @ fst i) n
10 ocaseval 
ocase z S @ n = recn z (\ i, S @ fst i) n
11 9, 10 ax_mp 
n, ocase z S @ n = n, recn z (\ i, S @ fst i) n
12 8, 11 ax_mp 
(\ i, S @ fst i) @ (n, ocase z S @ n) = (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n)
13 7, 12 ax_mp 
(\ i, S @ fst i) @ (n, ocase z S @ n) = S @ n -> (\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) = S @ n
14 fstpr 
fst (n, ocase z S @ n) = n
15 fsteq 
i = n, ocase z S @ n -> fst i = fst (n, ocase z S @ n)
16 14, 15 syl6eq 
i = n, ocase z S @ n -> fst i = n
17 16 appeq2d 
i = n, ocase z S @ n -> S @ fst i = S @ n
18 17 applame 
(\ i, S @ fst i) @ (n, ocase z S @ n) = S @ n
19 13, 18 ax_mp 
(\ i, S @ fst i) @ (n, recn z (\ i, S @ fst i) n) = S @ n
20 6, 19 ax_mp 
recn z (\ i, S @ fst i) (suc n) = S @ n
21 3, 20 ax_mp 
ocase z S @ suc n = S @ 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)