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 eqsidd 
_1 = n -> pset b == pset b
4 id 
_1 = n -> _1 = n
5 3, 4 appeqd 
_1 = n -> pset b @ _1 = pset b @ n
6 eqsidd 
_1 = n -> pset a == pset a
7 6, 4 appeqd 
_1 = n -> pset a @ _1 = pset a @ n
8 5, 7 eqeqd 
_1 = n -> (pset b @ _1 = pset a @ _1 <-> pset b @ n = pset a @ n)
9 eqsidd 
_1 = 0 -> pset b == pset b
10 id 
_1 = 0 -> _1 = 0
11 9, 10 appeqd 
_1 = 0 -> pset b @ _1 = pset b @ 0
12 eqsidd 
_1 = 0 -> pset a == pset a
13 12, 10 appeqd 
_1 = 0 -> pset a @ _1 = pset a @ 0
14 11, 13 eqeqd 
_1 = 0 -> (pset b @ _1 = pset a @ _1 <-> pset b @ 0 = pset a @ 0)
15 eqsidd 
_1 = a1 -> pset b == pset b
16 id 
_1 = a1 -> _1 = a1
17 15, 16 appeqd 
_1 = a1 -> pset b @ _1 = pset b @ a1
18 eqsidd 
_1 = a1 -> pset a == pset a
19 18, 16 appeqd 
_1 = a1 -> pset a @ _1 = pset a @ a1
20 17, 19 eqeqd 
_1 = a1 -> (pset b @ _1 = pset a @ _1 <-> pset b @ a1 = pset a @ a1)
21 eqsidd 
_1 = suc a1 -> pset b == pset b
22 id 
_1 = suc a1 -> _1 = suc a1
23 21, 22 appeqd 
_1 = suc a1 -> pset b @ _1 = pset b @ suc a1
24 eqsidd 
_1 = suc a1 -> pset a == pset a
25 24, 22 appeqd 
_1 = suc a1 -> pset a @ _1 = pset a @ suc a1
26 23, 25 eqeqd 
_1 = suc a1 -> (pset b @ _1 = pset a @ _1 <-> pset b @ suc a1 = pset a @ suc a1)
27 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
28 27 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
29 hyp h1 
G -> pset a @ 0 = z
30 29 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
31 28, 30 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
32 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
33 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))
34 lteq1 
i = a1 -> (i < n <-> a1 < n)
35 suceq 
i = a1 -> suc i = suc a1
36 35 appeq2d 
i = a1 -> pset b @ suc i = pset b @ suc a1
37 appeq2 
i = a1 -> pset b @ i = pset b @ a1
38 37 appeq2d 
i = a1 -> S @ (pset b @ i) = S @ (pset b @ a1)
39 36, 38 eqeqd 
i = a1 -> (pset b @ suc i = S @ (pset b @ i) <-> pset b @ suc a1 = S @ (pset b @ a1))
40 34, 39 imeqd 
i = a1 -> (i < n -> pset b @ suc i = S @ (pset b @ i) <-> a1 < n -> pset b @ suc a1 = S @ (pset b @ a1))
41 40 eale 
A. i (i < n -> pset b @ suc i = S @ (pset b @ i)) -> a1 < n -> pset b @ suc a1 = S @ (pset b @ a1)
42 41 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)
43 33, 42 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)
44 32, 43 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)
45 appeq2 
pset b @ a1 = pset a @ a1 -> S @ (pset b @ a1) = S @ (pset a @ a1)
46 45 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)
47 hyp h3 
G -> A. i (i < n -> pset a @ suc i = S @ (pset a @ i))
48 35 appeq2d 
i = a1 -> pset a @ suc i = pset a @ suc a1
49 appeq2 
i = a1 -> pset a @ i = pset a @ a1
50 49 appeq2d 
i = a1 -> S @ (pset a @ i) = S @ (pset a @ a1)
51 48, 50 eqeqd 
i = a1 -> (pset a @ suc i = S @ (pset a @ i) <-> pset a @ suc a1 = S @ (pset a @ a1))
52 34, 51 imeqd 
i = a1 -> (i < n -> pset a @ suc i = S @ (pset a @ i) <-> a1 < n -> pset a @ suc a1 = S @ (pset a @ a1))
53 52 eale 
A. i (i < n -> pset a @ suc i = S @ (pset a @ i)) -> a1 < n -> pset a @ suc a1 = S @ (pset a @ a1)
54 47, 53 rsyl 
G -> a1 < n -> pset a @ suc a1 = S @ (pset a @ a1)
55 54 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)
56 32, 55 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)
57 46, 56 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
58 44, 57 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
59 8, 14, 20, 26, 31, 58 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
60 hyp h2 
G -> pset a @ n = v
61 60 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
62 59, 61 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
63 2, 62 eqtr3d 
G /\ (pset b @ 0 = z /\ pset b @ n = u /\ A. i (i < n -> pset b @ suc i = S @ (pset b @ i))) -> u = v
64 63 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
65 pseteq 
b = a -> pset b == pset a
66 65 anwr 
G /\ u = v /\ b = a -> pset b == pset a
67 66 appeq1d 
G /\ u = v /\ b = a -> pset b @ 0 = pset a @ 0
68 29 anwll 
G /\ u = v /\ b = a -> pset a @ 0 = z
69 67, 68 eqtrd 
G /\ u = v /\ b = a -> pset b @ 0 = z
70 66 appeq1d 
G /\ u = v /\ b = a -> pset b @ n = pset a @ n
71 60 anwll 
G /\ u = v /\ b = a -> pset a @ n = v
72 anlr 
G /\ u = v /\ b = a -> u = v
73 71, 72 eqtr4d 
G /\ u = v /\ b = a -> pset a @ n = u
74 70, 73 eqtrd 
G /\ u = v /\ b = a -> pset b @ n = u
75 69, 74 iand 
G /\ u = v /\ b = a -> pset b @ 0 = z /\ pset b @ n = u
76 66 appeq1d 
G /\ u = v /\ b = a -> pset b @ suc i = pset a @ suc i
77 66 appeq1d 
G /\ u = v /\ b = a -> pset b @ i = pset a @ i
78 77 appeq2d 
G /\ u = v /\ b = a -> S @ (pset b @ i) = S @ (pset a @ i)
79 76, 78 eqeqd 
G /\ u = v /\ b = a -> (pset b @ suc i = S @ (pset b @ i) <-> pset a @ suc i = S @ (pset a @ i))
80 79 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))
81 80 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)))
82 47 anwll 
G /\ u = v /\ b = a -> A. i (i < n -> pset a @ suc i = S @ (pset a @ i))
83 81, 82 mpbird 
G /\ u = v /\ b = a -> A. i (i < n -> pset b @ suc i = S @ (pset b @ i))
84 75, 83 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))
85 84 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)))
86 85 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)))
87 64, 86 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)
88 87 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
89 88 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)