Theorem srecauxisf ≪ | index | src | ≫

theorem srecauxisf (S: set) (n: nat): $ isfun (srecaux S n) $;


x = n -> x = n
x = n -> srecaux S x = srecaux S n
x = n -> srecaux S x == srecaux S n
x = n -> (isfun (srecaux S x) <-> isfun (srecaux S n))
x = 0 -> x = 0
x = 0 -> srecaux S x = srecaux S 0
x = 0 -> srecaux S x == srecaux S 0
x = 0 -> (isfun (srecaux S x) <-> isfun (srecaux S 0))
x = y -> x = y
x = y -> srecaux S x = srecaux S y
x = y -> srecaux S x == srecaux S y
x = y -> (isfun (srecaux S x) <-> isfun (srecaux S y))
x = suc y -> x = suc y
x = suc y -> srecaux S x = srecaux S (suc y)
x = suc y -> srecaux S x == srecaux S (suc y)
x = suc y -> (isfun (srecaux S x) <-> isfun (srecaux S (suc y)))
srecaux S 0 == 0 -> (isfun (srecaux S 0) <-> isfun 0)
srecaux S 0 = 0 -> srecaux S 0 == 0
srecaux S 0 = 0
srecaux S 0 == 0
isfun (srecaux S 0) <-> isfun 0
isfun 0
isfun (srecaux S 0)
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y) -> (isfun (srecaux S (suc y)) <-> isfun (write (srecaux S y) y (S @ srecaux S y)))
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y)
isfun (srecaux S (suc y)) <-> isfun (write (srecaux S y) y (S @ srecaux S y))
isfun (srecaux S y) -> isfun (write (srecaux S y) y (S @ srecaux S y))
isfun (srecaux S y) -> isfun (srecaux S (suc y))
isfun (srecaux S n)

Step	Hyp	Ref	Expression
1		id	x = n -> x = n
2	1	srecauxeq2d	x = n -> srecaux S x = srecaux S n
3	2	nseqd	x = n -> srecaux S x == srecaux S n
4	3	isfeqd	x = n -> (isfun (srecaux S x) <-> isfun (srecaux S n))
5		id	x = 0 -> x = 0
6	5	srecauxeq2d	x = 0 -> srecaux S x = srecaux S 0
7	6	nseqd	x = 0 -> srecaux S x == srecaux S 0
8	7	isfeqd	x = 0 -> (isfun (srecaux S x) <-> isfun (srecaux S 0))
9		id	x = y -> x = y
10	9	srecauxeq2d	x = y -> srecaux S x = srecaux S y
11	10	nseqd	x = y -> srecaux S x == srecaux S y
12	11	isfeqd	x = y -> (isfun (srecaux S x) <-> isfun (srecaux S y))
13		id	x = suc y -> x = suc y
14	13	srecauxeq2d	x = suc y -> srecaux S x = srecaux S (suc y)
15	14	nseqd	x = suc y -> srecaux S x == srecaux S (suc y)
16	15	isfeqd	x = suc y -> (isfun (srecaux S x) <-> isfun (srecaux S (suc y)))
17		isfeq	srecaux S 0 == 0 -> (isfun (srecaux S 0) <-> isfun 0)
18		nseq	srecaux S 0 = 0 -> srecaux S 0 == 0
19		srecaux0	srecaux S 0 = 0
20	18, 19	ax_mp	srecaux S 0 == 0
21	17, 20	ax_mp	isfun (srecaux S 0) <-> isfun 0
22		isf0	isfun 0
23	21, 22	mpbir	isfun (srecaux S 0)
24		isfeq	srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y) -> (isfun (srecaux S (suc y)) <-> isfun (write (srecaux S y) y (S @ srecaux S y)))
25		srecauxS	srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y)
26	24, 25	ax_mp	isfun (srecaux S (suc y)) <-> isfun (write (srecaux S y) y (S @ srecaux S y))
27		writeisf	isfun (srecaux S y) -> isfun (write (srecaux S y) y (S @ srecaux S y))
28	26, 27	sylibr	isfun (srecaux S y) -> isfun (srecaux S (suc y))
29	4, 8, 12, 16, 23, 28	ind	isfun (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)