Theorem srecval ≪ | index | src | ≫

pub theorem srecval {i: nat} (S: set) (n: nat):
  $ srec S n = S @ (\. i e. upto n, srec S i) $;


srec S n = S @ srecaux S n -> S @ (\. i e. upto n, srec S i) = S @ srecaux S n -> srec S n = S @ (\. i e. upto n, srec S i)
srec S n = S @ srecaux S n
S @ (\. i e. upto n, srec S i) = S @ srecaux S n -> srec S n = S @ (\. i e. upto n, srec S i)
\. i e. upto n, srec S i = srecaux S n -> S @ (\. i e. upto n, srec S i) = S @ srecaux S n
\. i e. upto n, srec S i = lower (srecaux S n) -> lower (srecaux S n) = srecaux S n -> \. i e. upto n, srec S i = srecaux S n
(\ i, srec S i) |` upto n == srecaux S n -> lower ((\ i, srec S i) |` upto n) = lower (srecaux S n)
(\ i, srec S i) |` upto n == srecaux S n -> \. i e. upto n, srec S i = lower (srecaux S n)
(\ i, srec S i) |` upto n == srecaux S n
\. i e. upto n, srec S i = lower (srecaux S n)
lower (srecaux S n) = srecaux S n -> \. i e. upto n, srec S i = srecaux S n
lower (srecaux S n) = srecaux S n
\. i e. upto n, srec S i = srecaux S n
S @ (\. i e. upto n, srec S i) = S @ srecaux S n
srec S n = S @ (\. i e. upto n, srec S i)

Step	Hyp	Ref	Expression
1		eqtr4	srec S n = S @ srecaux S n -> S @ (\. i e. upto n, srec S i) = S @ srecaux S n -> srec S n = S @ (\. i e. upto n, srec S i)
2		srecval2	srec S n = S @ srecaux S n
3	1, 2	ax_mp	S @ (\. i e. upto n, srec S i) = S @ srecaux S n -> srec S n = S @ (\. i e. upto n, srec S i)
4		appeq2	\. i e. upto n, srec S i = srecaux S n -> S @ (\. i e. upto n, srec S i) = S @ srecaux S n
5		eqtr	\. i e. upto n, srec S i = lower (srecaux S n) -> lower (srecaux S n) = srecaux S n -> \. i e. upto n, srec S i = srecaux S n
6		lowereq	(\ i, srec S i) \|` upto n == srecaux S n -> lower ((\ i, srec S i) \|` upto n) = lower (srecaux S n)
7	6	conv rlam	(\ i, srec S i) \|` upto n == srecaux S n -> \. i e. upto n, srec S i = lower (srecaux S n)
8		srecres	(\ i, srec S i) \|` upto n == srecaux S n
9	7, 8	ax_mp	\. i e. upto n, srec S i = lower (srecaux S n)
10	5, 9	ax_mp	lower (srecaux S n) = srecaux S n -> \. i e. upto n, srec S i = srecaux S n
11		lowerns	lower (srecaux S n) = srecaux S n
12	10, 11	ax_mp	\. i e. upto n, srec S i = srecaux S n
13	4, 12	ax_mp	S @ (\. i e. upto n, srec S i) = S @ srecaux S n
14	3, 13	ax_mp	srec S n = S @ (\. i e. upto n, srec S i)

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)