Theorem listindd | index | src |

theorem listindd (G: wff) {x a l: nat} (n: nat) (px: wff x) (p0 pn: wff)
  (pl: wff l) (ps: wff a l):
  $ x = n -> (px <-> pn) $ >
  $ x = 0 -> (px <-> p0) $ >
  $ x = l -> (px <-> pl) $ >
  $ x = a : l -> (px <-> ps) $ >
  $ G -> p0 $ >
  $ G /\ pl -> ps $ >
  $ G -> pn $;
StepHypRefExpression
1 hyp hn
x = n -> (px <-> pn)
2 1 sbe
[n / x] px <-> pn
3 sbeq1
z = n -> ([z / x] px <-> [n / x] px)
4 2, 3 syl6bb
z = n -> ([z / x] px <-> pn)
5 sbeq1
z = w -> ([z / x] px <-> [w / x] px)
6 anr
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> w = 0
7 6 sbeq1d
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> ([w / x] px <-> [0 / x] px)
8 hyp h0
x = 0 -> (px <-> p0)
9 8 sbe
[0 / x] px <-> p0
10 hyp h1
G -> p0
11 9, 10 sylibr
G -> [0 / x] px
12 11 anwll
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> [0 / x] px
13 7, 12 mpbird
G /\ A. z (z < w -> [z / x] px) /\ w = 0 -> [w / x] px
14 excons
w != 0 <-> E. a E. l w = a : l
15 anr
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> ~w = 0
16 15 conv ne
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> w != 0
17 14, 16 sylib
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. a E. l w = a : l
18 hyp hs
x = a : l -> (px <-> ps)
19 18 sbe
[a : l / x] px <-> ps
20 anr
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> w = a : l
21 20 sbeq1d
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> ([w / x] px <-> [a : l / x] px)
22 19, 21 syl6bb
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> ([w / x] px <-> ps)
23 ltconsid2
l < a : l
24 20 lteq2d
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> (l < w <-> l < a : l)
25 23, 24 mpbiri
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> l < w
26 anlr
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> A. z (z < w -> [z / x] px)
27 lteq1
z = l -> (z < w <-> l < w)
28 hyp hl
x = l -> (px <-> pl)
29 28 sbe
[l / x] px <-> pl
30 sbeq1
z = l -> ([z / x] px <-> [l / x] px)
31 29, 30 syl6bb
z = l -> ([z / x] px <-> pl)
32 27, 31 imeqd
z = l -> (z < w -> [z / x] px <-> l < w -> pl)
33 32 eale
A. z (z < w -> [z / x] px) -> l < w -> pl
34 26, 33 rsyl
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> l < w -> pl
35 25, 34 mpd
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> pl
36 hyp h2
G /\ pl -> ps
37 36 exp
G -> pl -> ps
38 37 anwll
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> pl -> ps
39 35, 38 mpd
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> ps
40 22, 39 mpbird
G /\ A. z (z < w -> [z / x] px) /\ w = a : l -> [w / x] px
41 40 exp
G /\ A. z (z < w -> [z / x] px) -> w = a : l -> [w / x] px
42 41 anwl
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> w = a : l -> [w / x] px
43 42 eexd
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. l w = a : l -> [w / x] px
44 43 eexd
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. a E. l w = a : l -> [w / x] px
45 17, 44 mpd
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> [w / x] px
46 13, 45 casesda
G /\ A. z (z < w -> [z / x] px) -> [w / x] px
47 4, 5, 46 indstr
G -> pn

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)