Theorem rec0 ≪ | index | src | ≫

pub theorem rec0 (z: nat) (S: set): $ rec z S 0 = z $;

Step	Hyp	Ref	Expression
1		eqid	0 = 0
2		eqeq1	x = 0 -> (x = 0 <-> 0 = 0)
3		appeq2	x = 0 -> pset a @ x = pset a @ 0
4	3	eqeq1d	x = 0 -> (pset a @ x = z <-> pset a @ 0 = z)
5	2, 4	imeqd	x = 0 -> (x = 0 -> pset a @ x = z <-> 0 = 0 -> pset a @ 0 = z)
6	5	eale	A. x (x = 0 -> pset a @ x = z) -> 0 = 0 -> pset a @ 0 = z
7	1, 6	mpi	A. x (x = 0 -> pset a @ x = z) -> pset a @ 0 = z
8		absurd	~i < 0 -> i < 0 -> pset a @ suc i = S @ (pset a @ i)
9		lt02	~i < 0
10	8, 9	ax_mp	i < 0 -> pset a @ suc i = S @ (pset a @ i)
11	10	ax_gen	A. i (i < 0 -> pset a @ suc i = S @ (pset a @ i))
12	11	a1i	A. x (x = 0 -> pset a @ x = z) -> A. i (i < 0 -> pset a @ suc i = S @ (pset a @ i))
13	7, 7, 12	reclem	A. x (x = 0 -> pset a @ x = z) -> rec z S 0 = z
14	13	eex	E. a A. x (x = 0 -> pset a @ x = z) -> rec z S 0 = z
15		psetfn	finite {x \| x = 0} -> E. a A. x (x = 0 -> pset a @ x = z)
16		snfin	finite {x \| x = 0}
17	15, 16	ax_mp	E. a A. x (x = 0 -> pset a @ x = z)
18	14, 17	ax_mp	rec z S 0 = z

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)