Theorem receqd ≪ | index | src | ≫ 

theorem receqd (_G: wff) (_z1 _z2: nat) (_S1 _S2: set) (_n1 _n2: nat):
  $ _G -> _z1 = _z2 $ >
  $ _G -> _S1 == _S2 $ >
  $ _G -> _n1 = _n2 $ >
  $ _G -> rec _z1 _S1 _n1 = rec _z2 _S2 _n2 $;
StepHypRefExpression
1 eqidd 
_G -> pset a @ 0 = pset a @ 0
2 hyp _zh 
_G -> _z1 = _z2
3 1, 2 eqeqd 
_G -> (pset a @ 0 = _z1 <-> pset a @ 0 = _z2)
4 eqsidd 
_G -> pset a == pset a
5 hyp _nh 
_G -> _n1 = _n2
6 4, 5 appeqd 
_G -> pset a @ _n1 = pset a @ _n2
7 eqidd 
_G -> v = v
8 6, 7 eqeqd 
_G -> (pset a @ _n1 = v <-> pset a @ _n2 = v)
9 3, 8 aneqd 
_G -> (pset a @ 0 = _z1 /\ pset a @ _n1 = v <-> pset a @ 0 = _z2 /\ pset a @ _n2 = v)
10 eqidd 
_G -> i = i
11 10, 5 lteqd 
_G -> (i < _n1 <-> i < _n2)
12 eqidd 
_G -> pset a @ suc i = pset a @ suc i
13 hyp _Sh 
_G -> _S1 == _S2
14 eqidd 
_G -> pset a @ i = pset a @ i
15 13, 14 appeqd 
_G -> _S1 @ (pset a @ i) = _S2 @ (pset a @ i)
16 12, 15 eqeqd 
_G -> (pset a @ suc i = _S1 @ (pset a @ i) <-> pset a @ suc i = _S2 @ (pset a @ i))
17 11, 16 imeqd 
_G -> (i < _n1 -> pset a @ suc i = _S1 @ (pset a @ i) <-> i < _n2 -> pset a @ suc i = _S2 @ (pset a @ i))
18 17 aleqd 
_G -> (A. i (i < _n1 -> pset a @ suc i = _S1 @ (pset a @ i)) <-> A. i (i < _n2 -> pset a @ suc i = _S2 @ (pset a @ i)))
19 9, 18 aneqd 
_G ->
  (pset a @ 0 = _z1 /\ pset a @ _n1 = v /\ A. i (i < _n1 -> pset a @ suc i = _S1 @ (pset a @ i)) <->
    pset a @ 0 = _z2 /\ pset a @ _n2 = v /\ A. i (i < _n2 -> pset a @ suc i = _S2 @ (pset a @ i)))
20 19 exeqd 
_G ->
  (E. a (pset a @ 0 = _z1 /\ pset a @ _n1 = v /\ A. i (i < _n1 -> pset a @ suc i = _S1 @ (pset a @ i))) <->
    E. a (pset a @ 0 = _z2 /\ pset a @ _n2 = v /\ A. i (i < _n2 -> pset a @ suc i = _S2 @ (pset a @ i))))
21 20 abeqd 
_G ->
  {v | E. a (pset a @ 0 = _z1 /\ pset a @ _n1 = v /\ A. i (i < _n1 -> pset a @ suc i = _S1 @ (pset a @ i)))} ==
    {v | E. a (pset a @ 0 = _z2 /\ pset a @ _n2 = v /\ A. i (i < _n2 -> pset a @ suc i = _S2 @ (pset a @ i)))}
22 21 theeqd 
_G ->
  the {v | E. a (pset a @ 0 = _z1 /\ pset a @ _n1 = v /\ A. i (i < _n1 -> pset a @ suc i = _S1 @ (pset a @ i)))} =
    the {v | E. a (pset a @ 0 = _z2 /\ pset a @ _n2 = v /\ A. i (i < _n2 -> pset a @ suc i = _S2 @ (pset a @ i)))}
23 22 conv rec 
_G -> rec _z1 _S1 _n1 = rec _z2 _S2 _n2

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, addeq, muleq)