Theorem reclem ≪ | index | src | ≫ 

theorem reclem (G: wff) (S: set) (a n v z: nat) {i: nat}:
  $ G -> pset a @ 0 = z $ >
  $ G -> pset a @ n = v $ >
  $ G -> A. i (i < n -> pset a @ suc i = S @ (pset a @ i)) $ >
  $ G -> rec z S n = v $;
StepHypRefExpression
1 anlr 
pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i)) -> pset b @ n = u
2 1 anwr 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset b @ n = u
3 id 
_1 = n -> _1 = n
4 3 appeq2d 
_1 = n -> pset b @ _1 = pset b @ n
5 3 appeq2d 
_1 = n -> pset a @ _1 = pset a @ n
6 4, 5 eqeqd 
_1 = n -> (pset b @ _1 = pset a @ _1 <-> pset b @ n = pset a @ n)
7 id 
_1 = 0 -> _1 = 0
8 7 appeq2d 
_1 = 0 -> pset b @ _1 = pset b @ 0
9 7 appeq2d 
_1 = 0 -> pset a @ _1 = pset a @ 0
10 8, 9 eqeqd 
_1 = 0 -> (pset b @ _1 = pset a @ _1 <-> pset b @ 0 = pset a @ 0)
11 id 
_1 = a1 -> _1 = a1
12 11 appeq2d 
_1 = a1 -> pset b @ _1 = pset b @ a1
13 11 appeq2d 
_1 = a1 -> pset a @ _1 = pset a @ a1
14 12, 13 eqeqd 
_1 = a1 -> (pset b @ _1 = pset a @ _1 <-> pset b @ a1 = pset a @ a1)
15 id 
_1 = suc a1 -> _1 = suc a1
16 15 appeq2d 
_1 = suc a1 -> pset b @ _1 = pset b @ suc a1
17 15 appeq2d 
_1 = suc a1 -> pset a @ _1 = pset a @ suc a1
18 16, 17 eqeqd 
_1 = suc a1 -> (pset b @ _1 = pset a @ _1 <-> pset b @ suc a1 = pset a @ suc a1)
19 anll 
pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i)) -> pset b @ 0 = z
20 19 anwr 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset b @ 0 = z
21 hyp h1 
G -> pset a @ 0 = z
22 21 anwl 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset a @ 0 = z
23 20, 22 eqtr4d 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset b @ 0 = pset a @ 0
24 anlr 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 -> a1 < n
25 anllr 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))
26 lteq1 
i = a1 -> (i < n <-> a1 < n)
27 suceq 
i = a1 -> suc i = suc a1
28 27 appeq2d 
i = a1 -> pset b @ suc i = pset b @ suc a1
29 appeq2 
i = a1 -> pset b @ i = pset b @ a1
30 29 appeq2d 
i = a1 -> S @ (pset b @ i) = S @ (pset b @ a1)
31 28, 30 eqeqd 
i = a1 -> (pset b @ suc i = S @ (pset b @ i) <-> pset b @ suc a1 = S @ (pset b @ a1))
32 26, 31 imeqd 
i = a1 -> (i < n -> pset b @ suc i = S @ (pset b @ i) <-> a1 < n -> pset b @ suc a1 = S @ (pset b @ a1))
33 32 eale 
A. i (i < n -> pset b @ suc i = S @ (pset b @ i)) -> a1 < n -> pset b @ suc a1 = S @ (pset b @ a1)
34 33 anwr 
pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i)) -> a1 < n -> pset b @ suc a1 = S @ (pset b @ a1)
35 25, 34 rsyl 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  a1 < n ->
  pset b @ suc a1 = S @ (pset b @ a1)
36 24, 35 mpd 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  pset b @ suc a1 = S @ (pset b @ a1)
37 appeq2 
pset b @ a1 = pset a @ a1 -> S @ (pset b @ a1) = S @ (pset a @ a1)
38 37 anwr 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  S @ (pset b @ a1) = S @ (pset a @ a1)
39 hyp h3 
G -> A. i (i < n -> pset a @ suc i = S @ (pset a @ i))
40 27 appeq2d 
i = a1 -> pset a @ suc i = pset a @ suc a1
41 appeq2 
i = a1 -> pset a @ i = pset a @ a1
42 41 appeq2d 
i = a1 -> S @ (pset a @ i) = S @ (pset a @ a1)
43 40, 42 eqeqd 
i = a1 -> (pset a @ suc i = S @ (pset a @ i) <-> pset a @ suc a1 = S @ (pset a @ a1))
44 26, 43 imeqd 
i = a1 -> (i < n -> pset a @ suc i = S @ (pset a @ i) <-> a1 < n -> pset a @ suc a1 = S @ (pset a @ a1))
45 44 eale 
A. i (i < n -> pset a @ suc i = S @ (pset a @ i)) -> a1 < n -> pset a @ suc a1 = S @ (pset a @ a1)
46 39, 45 rsyl 
G -> a1 < n -> pset a @ suc a1 = S @ (pset a @ a1)
47 46 anw3l 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  a1 < n ->
  pset a @ suc a1 = S @ (pset a @ a1)
48 24, 47 mpd 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  pset a @ suc a1 = S @ (pset a @ a1)
49 38, 48 eqtr4d 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  S @ (pset b @ a1) = pset a @ suc a1
50 36, 49 eqtrd 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) /\ a1 < n /\ pset b @ a1 = pset a @ a1 ->
  pset b @ suc a1 = pset a @ suc a1
51 6, 10, 14, 18, 23, 50 indlt 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset b @ n = pset a @ n
52 hyp h2 
G -> pset a @ n = v
53 52 anwl 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset a @ n = v
54 51, 53 eqtrd 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> pset b @ n = v
55 2, 54 eqtr3d 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> u = v
56 55 eexda 
G -> E. b (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> u = v
57 pseteq 
b = a -> pset b == pset a
58 57 anwr 
G /\ u = v /\ b = a -> pset b == pset a
59 58 appeq1d 
G /\ u = v /\ b = a -> pset b @ 0 = pset a @ 0
60 21 anwll 
G /\ u = v /\ b = a -> pset a @ 0 = z
61 59, 60 eqtrd 
G /\ u = v /\ b = a -> pset b @ 0 = z
62 58 appeq1d 
G /\ u = v /\ b = a -> pset b @ n = pset a @ n
63 52 anwll 
G /\ u = v /\ b = a -> pset a @ n = v
64 anlr 
G /\ u = v /\ b = a -> u = v
65 63, 64 eqtr4d 
G /\ u = v /\ b = a -> pset a @ n = u
66 62, 65 eqtrd 
G /\ u = v /\ b = a -> pset b @ n = u
67 61, 66 iand 
G /\ u = v /\ b = a -> pset b @ 0 = z /\ pset b @ n = u
68 58 appeq1d 
G /\ u = v /\ b = a -> pset b @ suc i = pset a @ suc i
69 58 appeq1d 
G /\ u = v /\ b = a -> pset b @ i = pset a @ i
70 69 appeq2d 
G /\ u = v /\ b = a -> S @ (pset b @ i) = S @ (pset a @ i)
71 68, 70 eqeqd 
G /\ u = v /\ b = a -> (pset b @ suc i = S @ (pset b @ i) <-> pset a @ suc i = S @ (pset a @ i))
72 71 imeq2d 
G /\ u = v /\ b = a -> (i < n -> pset b @ suc i = S @ (pset b @ i) <-> i < n -> pset a @ suc i = S @ (pset a @ i))
73 72 aleqd 
G /\ u = v /\ b = a -> (A. i (i < n -> pset b @ suc i = S @ (pset b @ i)) <-> A. i (i < n -> pset a @ suc i = S @ (pset a @ i)))
74 39 anwll 
G /\ u = v /\ b = a -> A. i (i < n -> pset a @ suc i = S @ (pset a @ i))
75 73, 74 mpbird 
G /\ u = v /\ b = a -> A. i (i < n -> pset b @ suc i = S @ (pset b @ i))
76 67, 75 iand 
G /\ u = v /\ b = a -> pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))
77 76 iexde 
G /\ u = v -> E. b (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i)))
78 77 exp 
G -> u = v -> E. b (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i)))
79 56, 78 ibid 
G -> (E. b (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) <-> u = v)
80 79 eqtheabd 
G -> the {u | E. b (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i)))} = v
81 80 conv rec 
G -> rec z S n = v

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 (peano2, peano5, addeq, muleq, add0, addS)