Theorem srecres ≪ | index | src | ≫ 

theorem srecres (S: set) {i: nat} (n: nat):
  $ (\ i, srec S i) |` upto n == srecaux S n $;
StepHypRefExpression
1 eqstr3 
(\ i, srecaux S n @ i) |` upto n == (\ i, srec S i) |` upto n -> (\ i, srecaux S n @ i) |` upto n == srecaux S n -> (\ i, srec S i) |` upto n == srecaux S n
2 reslameq 
A. i (i e. upto n -> srecaux S n @ i = srec S i) -> (\ i, srecaux S n @ i) |` upto n == (\ i, srec S i) |` upto n
3 elupto 
i e. upto n <-> i < n
4 srecauxapp 
i < n -> srecaux S n @ i = srec S i
5 3, 4 sylbi 
i e. upto n -> srecaux S n @ i = srec S i
6 5 ax_gen 
A. i (i e. upto n -> srecaux S n @ i = srec S i)
7 2, 6 ax_mp 
(\ i, srecaux S n @ i) |` upto n == (\ i, srec S i) |` upto n
8 1, 7 ax_mp 
(\ i, srecaux S n @ i) |` upto n == srecaux S n -> (\ i, srec S i) |` upto n == srecaux S n
9 eqstr3 
(\ i, srecaux S n @ i) |` Dom (srecaux S n) == (\ i, srecaux S n @ i) |` upto n ->
  (\ i, srecaux S n @ i) |` Dom (srecaux S n) == srecaux S n ->
  (\ i, srecaux S n @ i) |` upto n == srecaux S n
10 reseq2 
Dom (srecaux S n) == upto n -> (\ i, srecaux S n @ i) |` Dom (srecaux S n) == (\ i, srecaux S n @ i) |` upto n
11 dmsrecaux 
Dom (srecaux S n) == upto n
12 10, 11 ax_mp 
(\ i, srecaux S n @ i) |` Dom (srecaux S n) == (\ i, srecaux S n @ i) |` upto n
13 9, 12 ax_mp 
(\ i, srecaux S n @ i) |` Dom (srecaux S n) == srecaux S n -> (\ i, srecaux S n @ i) |` upto n == srecaux S n
14 lamapp 
(\ i, srecaux S n @ i) |` Dom (srecaux S n) == srecaux S n <-> isfun (srecaux S n)
15 srecauxisf 
isfun (srecaux S n)
16 14, 15 mpbir 
(\ i, srecaux S n @ i) |` Dom (srecaux S n) == srecaux S n
17 13, 16 ax_mp 
(\ i, srecaux S n @ i) |` upto n == srecaux S n
18 8, 17 ax_mp 
(\ i, srec S i) |` upto n == srecaux 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)