Theorem srecauxisf ≪ | index | src | ≫

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


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