Theorem lfnS ≪ | index | src | ≫ 

theorem lfnS (F: set) {i: nat} (n: nat):
  $ lfn F (suc n) = F @ 0 : lfn (\ i, F @ suc i) n $;
StepHypRefExpression
1 eqtr4 
lfn F (suc n) = F @ 0 : lfnaux F (suc 0) n -> F @ 0 : lfn (\ i, F @ suc i) n = F @ 0 : lfnaux F (suc 0) n -> lfn F (suc n) = F @ 0 : lfn (\ i, F @ suc i) n
2 lfnauxS 
lfnaux F 0 (suc n) = F @ 0 : lfnaux F (suc 0) n
3 2 conv lfn 
lfn F (suc n) = F @ 0 : lfnaux F (suc 0) n
4 1, 3 ax_mp 
F @ 0 : lfn (\ i, F @ suc i) n = F @ 0 : lfnaux F (suc 0) n -> lfn F (suc n) = F @ 0 : lfn (\ i, F @ suc i) n
5 conseq2 
lfn (\ i, F @ suc i) n = lfnaux F (suc 0) n -> F @ 0 : lfn (\ i, F @ suc i) n = F @ 0 : lfnaux F (suc 0) n
6 lfnauxshift 
A. a1 (\ i, F @ suc i) @ (0 + a1) = F @ (suc 0 + a1) -> lfnaux (\ i, F @ suc i) 0 n = lfnaux F (suc 0) n
7 6 conv lfn 
A. a1 (\ i, F @ suc i) @ (0 + a1) = F @ (suc 0 + a1) -> lfn (\ i, F @ suc i) n = lfnaux F (suc 0) n
8 addS1 
suc 0 + a1 = suc (0 + a1)
9 suceq 
i = 0 + a1 -> suc i = suc (0 + a1)
10 8, 9 syl6eqr 
i = 0 + a1 -> suc i = suc 0 + a1
11 10 appeq2d 
i = 0 + a1 -> F @ suc i = F @ (suc 0 + a1)
12 11 applame 
(\ i, F @ suc i) @ (0 + a1) = F @ (suc 0 + a1)
13 12 ax_gen 
A. a1 (\ i, F @ suc i) @ (0 + a1) = F @ (suc 0 + a1)
14 7, 13 ax_mp 
lfn (\ i, F @ suc i) n = lfnaux F (suc 0) n
15 5, 14 ax_mp 
F @ 0 : lfn (\ i, F @ suc i) n = F @ 0 : lfnaux F (suc 0) n
16 4, 15 ax_mp 
lfn F (suc n) = F @ 0 : lfn (\ i, F @ suc i) 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)