recS - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		suceq	m = n -> suc m = suc n
2	1	receq3d	m = n -> rec z S (suc m) = rec z S (suc n)
3		receq3	m = n -> rec z S m = rec z S n
4	3	appeq2d	m = n -> S @ rec z S m = S @ rec z S n
5	2, 4	eqeqd	m = n -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc n) = S @ rec z S n)
6		suceq	m = k -> suc m = suc k
7	6	receq3d	m = k -> rec z S (suc m) = rec z S (suc k)
8		receq3	m = k -> rec z S m = rec z S k
9	8	appeq2d	m = k -> S @ rec z S m = S @ rec z S k
10	7, 9	eqeqd	m = k -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc k) = S @ rec z S k)
11		psetfn	finite {x \| x <= suc k} -> E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
12		lefin	finite {x \| x <= suc k}
13	11, 12	ax_mp	E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
14		rec0	rec z S 0 = z
15		le01	0 <= suc k
16		leeq1	x = 0 -> (x <= suc k <-> 0 <= suc k)
17		appeq2	x = 0 -> pset a @ x = pset a @ 0
18		ifneg	~x = suc k -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x
19		con2	(x = suc k -> ~x = 0) -> x = 0 -> ~x = suc k
20		sucne0	x = suc k -> x != 0
21	20	conv ne	x = suc k -> ~x = 0
22	19, 21	ax_mp	x = 0 -> ~x = suc k
23	18, 22	syl	x = 0 -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x
24		receq3	x = 0 -> rec z S x = rec z S 0
25	23, 24	eqtrd	x = 0 -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S 0
26	17, 25	eqeqd	x = 0 -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ 0 = rec z S 0)
27	16, 26	imeqd	x = 0 -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> 0 <= suc k -> pset a @ 0 = rec z S 0)
28	27	eale	A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> 0 <= suc k -> pset a @ 0 = rec z S 0
29	15, 28	mpi	A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = rec z S 0
30	14, 29	syl6eq	A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = z
31	30	anwr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = z
32		leid	suc k <= suc k
33		leeq1	x = suc k -> (x <= suc k <-> suc k <= suc k)
34		appeq2	x = suc k -> pset a @ x = pset a @ suc k
35		ifpos	x = suc k -> if (x = suc k) (S @ rec z S k) (rec z S x) = S @ rec z S k
36	34, 35	eqeqd	x = suc k -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ suc k = S @ rec z S k)
37	33, 36	imeqd	x = suc k -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> suc k <= suc k -> pset a @ suc k = S @ rec z S k)
38	37	eale	A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> suc k <= suc k -> pset a @ suc k = S @ rec z S k
39	32, 38	mpi	A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ suc k = S @ rec z S k
40	39	anwr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ suc k = S @ rec z S k
41		leltsuc	y <= k <-> y < suc k
42		lesuc	y <= k <-> suc y <= suc k
43		anr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> y <= k
44	42, 43	sylib	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> suc y <= suc k
45		anlr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
46		leeq1	x = suc y -> (x <= suc k <-> suc y <= suc k)
47		appeq2	x = suc y -> pset a @ x = pset a @ suc y
48		peano2	suc y = suc k <-> y = k
49		eqeq1	x = suc y -> (x = suc k <-> suc y = suc k)
50	48, 49	syl6bb	x = suc y -> (x = suc k <-> y = k)
51		eqidd	x = suc y -> S @ rec z S k = S @ rec z S k
52		receq3	x = suc y -> rec z S x = rec z S (suc y)
53	50, 51, 52	ifeqd	x = suc y -> if (x = suc k) (S @ rec z S k) (rec z S x) = if (y = k) (S @ rec z S k) (rec z S (suc y))
54	47, 53	eqeqd	x = suc y -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y)))
55	46, 54	imeqd	x = suc y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y)))
56	55	eale	A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))
57	45, 56	rsyl	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))
58	44, 57	mpd	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))
59		ifpos	y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ rec z S k
60	59	anwr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ rec z S k
61		eqcom	pset a @ y = rec z S y -> rec z S y = pset a @ y
62		biim1	x <= suc k -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
63		leeq1	x = y -> (x <= suc k <-> y <= suc k)
64	63	anwr	y <= k /\ x = y -> (x <= suc k <-> y <= suc k)
65		anl	y <= k /\ x = y -> y <= k
66		lesucid	k <= suc k
67	66	a1i	y <= k /\ x = y -> k <= suc k
68	65, 67	letrd	y <= k /\ x = y -> y <= suc k
69	64, 68	mpbird	y <= k /\ x = y -> x <= suc k
70	62, 69	syl	y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))
71		appeq2	x = y -> pset a @ x = pset a @ y
72	71	anwr	y <= k /\ x = y -> pset a @ x = pset a @ y
73		ltne	x < suc k -> x != suc k
74	73	conv ne	x < suc k -> ~x = suc k
75		leltsuc	x <= k <-> x < suc k
76		leeq1	x = y -> (x <= k <-> y <= k)
77		id	y <= k -> y <= k
78	76, 77	syl5ibrcom	y <= k -> x = y -> x <= k
79	78	imp	y <= k /\ x = y -> x <= k
80	75, 79	sylib	y <= k /\ x = y -> x < suc k
81	74, 80	syl	y <= k /\ x = y -> ~x = suc k
82	18, 81	syl	y <= k /\ x = y -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x
83		receq3	x = y -> rec z S x = rec z S y
84	83	anwr	y <= k /\ x = y -> rec z S x = rec z S y
85	82, 84	eqtrd	y <= k /\ x = y -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S y
86	72, 85	eqeqd	y <= k /\ x = y -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ y = rec z S y)
87	70, 86	bitrd	y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ y = rec z S y)
88	87	bi1d	y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ y = rec z S y
89	61, 88	syl6	y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y
90	89	ealde	y <= k -> A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y
91	90	anwr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y
92	45, 91	mpd	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> rec z S y = pset a @ y
93	92	anwl	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k -> rec z S y = pset a @ y
94		receq3	y = k -> rec z S y = rec z S k
95	94	anwr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k -> rec z S y = rec z S k
96	93, 95	eqtr3d	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k -> pset a @ y = rec z S k
97	96	appeq2d	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k -> S @ (pset a @ y) = S @ rec z S k
98	60, 97	eqtr4d	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)
99		ifneg	~y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = rec z S (suc y)
100	99	anwr	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = rec z S (suc y)
101		orcom	y < k \/ y = k -> y = k \/ y < k
102	101	conv or	y < k \/ y = k -> ~y = k -> y < k
103		leloe	y <= k <-> y < k \/ y = k
104	103, 43	sylib	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> y < k \/ y = k
105	102, 104	syl	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> ~y = k -> y < k
106	105	imp	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> y < k
107		an3l	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> A. m (m < k -> rec z S (suc m) = S @ rec z S m)
108		lteq1	m = y -> (m < k <-> y < k)
109		suceq	m = y -> suc m = suc y
110	109	receq3d	m = y -> rec z S (suc m) = rec z S (suc y)
111		receq3	m = y -> rec z S m = rec z S y
112	111	appeq2d	m = y -> S @ rec z S m = S @ rec z S y
113	110, 112	eqeqd	m = y -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc y) = S @ rec z S y)
114	108, 113	imeqd	m = y -> (m < k -> rec z S (suc m) = S @ rec z S m <-> y < k -> rec z S (suc y) = S @ rec z S y)
115	114	eale	A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> y < k -> rec z S (suc y) = S @ rec z S y
116	107, 115	rsyl	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> y < k -> rec z S (suc y) = S @ rec z S y
117	106, 116	mpd	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> rec z S (suc y) = S @ rec z S y
118	92	anwl	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> rec z S y = pset a @ y
119	118	appeq2d	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> S @ rec z S y = S @ (pset a @ y)
120	117, 119	eqtrd	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> rec z S (suc y) = S @ (pset a @ y)
121	100, 120	eqtrd	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)
122	98, 121	casesda	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)
123	58, 122	eqtrd	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> pset a @ suc y = S @ (pset a @ y)
124	123	exp	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> y <= k -> pset a @ suc y = S @ (pset a @ y)
125	41, 124	syl5bir	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> y < suc k -> pset a @ suc y = S @ (pset a @ y)
126	125	iald	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> A. y (y < suc k -> pset a @ suc y = S @ (pset a @ y))
127	31, 40, 126	reclem	A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S (suc k) = S @ rec z S k
128	127	eexda	A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S (suc k) = S @ rec z S k
129	13, 128	mpi	A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> rec z S (suc k) = S @ rec z S k
130	129	anwr	T. /\ A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> rec z S (suc k) = S @ rec z S k
131	5, 10, 130	indstr	T. -> rec z S (suc n) = S @ rec z S n
132	131	trud	rec z S (suc n) = S @ rec z S n

1

m = n -> suc m = suc n

2

1

receq3d

m = n -> rec z S (suc m) = rec z S (suc n)

3

receq3

m = n -> rec z S m = rec z S n

4

3

appeq2d

m = n -> S @ rec z S m = S @ rec z S n

5

2, 4

eqeqd

m = n -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc n) = S @ rec z S n)

6

suceq

m = k -> suc m = suc k

7

6

receq3d

m = k -> rec z S (suc m) = rec z S (suc k)

8

receq3

m = k -> rec z S m = rec z S k

9

8

appeq2d

m = k -> S @ rec z S m = S @ rec z S k

10

7, 9

eqeqd

m = k -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc k) = S @ rec z S k)

11

psetfn

finite {x | x <= suc k} -> E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))

12

lefin

finite {x | x <= suc k}

13

11, 12

ax_mp

E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))

14

rec0

rec z S 0 = z

15

le01

0 <= suc k

16

leeq1

x = 0 -> (x <= suc k <-> 0 <= suc k)

17

appeq2

x = 0 -> pset a @ x = pset a @ 0

18

ifneg

~x = suc k -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x

19

con2

(x = suc k -> ~x = 0) -> x = 0 -> ~x = suc k

20

sucne0

x = suc k -> x != 0

22

19, 21

ax_mp

x = 0 -> ~x = suc k

23

18, 22

syl

x = 0 -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x

24

receq3

x = 0 -> rec z S x = rec z S 0

25

23, 24

eqtrd

x = 0 -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S 0

26

17, 25

eqeqd

x = 0 -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ 0 = rec z S 0)

27

16, 26

imeqd

x = 0 -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> 0 <= suc k -> pset a @ 0 = rec z S 0)

28

27

eale

A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> 0 <= suc k -> pset a @ 0 = rec z S 0

29

15, 28

mpi

A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = rec z S 0

30

14, 29

syl6eq

A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = z

31

30

anwr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ 0 = z

32

leid

suc k <= suc k

33

leeq1

x = suc k -> (x <= suc k <-> suc k <= suc k)

34

appeq2

x = suc k -> pset a @ x = pset a @ suc k

35

ifpos

x = suc k -> if (x = suc k) (S @ rec z S k) (rec z S x) = S @ rec z S k

36

34, 35

eqeqd

x = suc k -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ suc k = S @ rec z S k)

37

33, 36

imeqd

x = suc k -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> suc k <= suc k -> pset a @ suc k = S @ rec z S k)

38

37

eale

A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> suc k <= suc k -> pset a @ suc k = S @ rec z S k

39

32, 38

mpi

A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ suc k = S @ rec z S k

40

39

anwr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  pset a @ suc k = S @ rec z S k

41

leltsuc

y <= k <-> y < suc k

42

lesuc

y <= k <-> suc y <= suc k

43

anr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> y <= k

44

42, 43

sylib

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> suc y <= suc k

45

anlr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))

46

leeq1

x = suc y -> (x <= suc k <-> suc y <= suc k)

47

appeq2

x = suc y -> pset a @ x = pset a @ suc y

48

peano2

suc y = suc k <-> y = k

49

eqeq1

x = suc y -> (x = suc k <-> suc y = suc k)

50

48, 49

syl6bb

x = suc y -> (x = suc k <-> y = k)

51

eqidd

x = suc y -> S @ rec z S k = S @ rec z S k

52

receq3

x = suc y -> rec z S x = rec z S (suc y)

53

50, 51, 52

ifeqd

x = suc y -> if (x = suc k) (S @ rec z S k) (rec z S x) = if (y = k) (S @ rec z S k) (rec z S (suc y))

54

47, 53

eqeqd

x = suc y -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y)))

55

46, 54

imeqd

x = suc y ->
  (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y)))

56

55

eale

A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> suc y <= suc k -> pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))

57

45, 56

rsyl

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  suc y <= suc k ->
  pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))

58

44, 57

mpd

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  pset a @ suc y = if (y = k) (S @ rec z S k) (rec z S (suc y))

59

ifpos

y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ rec z S k

60

59

anwr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ rec z S k

61

eqcom

pset a @ y = rec z S y -> rec z S y = pset a @ y

62

biim1

x <= suc k -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))

63

leeq1

x = y -> (x <= suc k <-> y <= suc k)

64

63

anwr

y <= k /\ x = y -> (x <= suc k <-> y <= suc k)

65

anl

y <= k /\ x = y -> y <= k

66

lesucid

k <= suc k

67

66

a1i

y <= k /\ x = y -> k <= suc k

68

65, 67

letrd

y <= k /\ x = y -> y <= suc k

69

64, 68

mpbird

y <= k /\ x = y -> x <= suc k

70

62, 69

syl

y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x))

71

appeq2

x = y -> pset a @ x = pset a @ y

72

71

anwr

y <= k /\ x = y -> pset a @ x = pset a @ y

73

ltne

x < suc k -> x != suc k

75

leltsuc

x <= k <-> x < suc k

76

leeq1

x = y -> (x <= k <-> y <= k)

77

id

y <= k -> y <= k

78

76, 77

syl5ibrcom

y <= k -> x = y -> x <= k

79

78

imp

y <= k /\ x = y -> x <= k

80

75, 79

sylib

y <= k /\ x = y -> x < suc k

81

74, 80

syl

y <= k /\ x = y -> ~x = suc k

82

18, 81

syl

y <= k /\ x = y -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S x

83

receq3

x = y -> rec z S x = rec z S y

84

83

anwr

y <= k /\ x = y -> rec z S x = rec z S y

85

82, 84

eqtrd

y <= k /\ x = y -> if (x = suc k) (S @ rec z S k) (rec z S x) = rec z S y

86

72, 85

eqeqd

y <= k /\ x = y -> (pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ y = rec z S y)

87

70, 86

bitrd

y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x) <-> pset a @ y = rec z S y)

88

87

bi1d

y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> pset a @ y = rec z S y

89

61, 88

syl6

y <= k /\ x = y -> (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y

90

89

ealde

y <= k -> A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) -> rec z S y = pset a @ y

91

90

anwr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  rec z S y = pset a @ y

92

45, 91

mpd

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  rec z S y = pset a @ y

93

92

anwl

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  rec z S y = pset a @ y

94

receq3

y = k -> rec z S y = rec z S k

95

94

anwr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  rec z S y = rec z S k

96

93, 95

eqtr3d

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  pset a @ y = rec z S k

97

96

appeq2d

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  S @ (pset a @ y) = S @ rec z S k

98

60, 97

eqtr4d

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)

99

ifneg

~y = k -> if (y = k) (S @ rec z S k) (rec z S (suc y)) = rec z S (suc y)

100

99

anwr

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = rec z S (suc y)

101

orcom

y < k \/ y = k -> y = k \/ y < k

103

leloe

y <= k <-> y < k \/ y = k

104

103, 43

sylib

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> y < k \/ y = k

105

102, 104

syl

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k -> ~y = k -> y < k

106

105

imp

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k -> y < k

107

an3l

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  A. m (m < k -> rec z S (suc m) = S @ rec z S m)

108

lteq1

m = y -> (m < k <-> y < k)

109

suceq

m = y -> suc m = suc y

110

109

receq3d

m = y -> rec z S (suc m) = rec z S (suc y)

111

receq3

m = y -> rec z S m = rec z S y

112

111

appeq2d

m = y -> S @ rec z S m = S @ rec z S y

113

110, 112

eqeqd

m = y -> (rec z S (suc m) = S @ rec z S m <-> rec z S (suc y) = S @ rec z S y)

114

108, 113

imeqd

m = y -> (m < k -> rec z S (suc m) = S @ rec z S m <-> y < k -> rec z S (suc y) = S @ rec z S y)

115

114

eale

A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> y < k -> rec z S (suc y) = S @ rec z S y

116

107, 115

rsyl

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  y < k ->
  rec z S (suc y) = S @ rec z S y

117

106, 116

mpd

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  rec z S (suc y) = S @ rec z S y

118

92

anwl

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  rec z S y = pset a @ y

119

118

appeq2d

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  S @ rec z S y = S @ (pset a @ y)

120

117, 119

eqtrd

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  rec z S (suc y) = S @ (pset a @ y)

121

100, 120

eqtrd

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k /\ ~y = k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)

122

98, 121

casesda

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  if (y = k) (S @ rec z S k) (rec z S (suc y)) = S @ (pset a @ y)

123

58, 122

eqtrd

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) /\ y <= k ->
  pset a @ suc y = S @ (pset a @ y)

124

123

exp

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  y <= k ->
  pset a @ suc y = S @ (pset a @ y)

125

41, 124

syl5bir

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  y < suc k ->
  pset a @ suc y = S @ (pset a @ y)

126

125

iald

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  A. y (y < suc k -> pset a @ suc y = S @ (pset a @ y))

127

31, 40, 126

reclem

A. m (m < k -> rec z S (suc m) = S @ rec z S m) /\ A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  rec z S (suc k) = S @ rec z S k

128

127

eexda

A. m (m < k -> rec z S (suc m) = S @ rec z S m) ->
  E. a A. x (x <= suc k -> pset a @ x = if (x = suc k) (S @ rec z S k) (rec z S x)) ->
  rec z S (suc k) = S @ rec z S k

129

13, 128

mpi

A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> rec z S (suc k) = S @ rec z S k

130

129

anwr

T. /\ A. m (m < k -> rec z S (suc m) = S @ rec z S m) -> rec z S (suc k) = S @ rec z S k

131

5, 10, 130

indstr

T. -> rec z S (suc n) = S @ rec z S n

132

131

trud

rec z S (suc n) = S @ rec z S n

Theorem recS ≪ | index | src | ≫

Axiom use