Theorem rlistindd ≪ | index | src | ≫ 

theorem rlistindd (G: wff) {x l a: nat} (n: nat) (px: wff x) (p0 pn: wff)
  (pl: wff l) (ps: wff l a):
  $ x = n -> (px <-> pn) $ >
  $ x = 0 -> (px <-> p0) $ >
  $ x = l -> (px <-> pl) $ >
  $ x = l |> a -> (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 exsnoc 
w != 0 <-> E. l E. a w = l |> a
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. l E. a w = l |> a
18 hyp hs 
x = l |> a -> (px <-> ps)
19 18 sbe 
[l |> a / x] px <-> ps
20 anr 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> w = l |> a
21 20 sbeq1d 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> ([w / x] px <-> [l |> a / x] px)
22 19, 21 syl6bb 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> ([w / x] px <-> ps)
23 snoclt 
l < l |> a
24 20 lteq2d 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> (l < w <-> l < l |> a)
25 23, 24 mpbiri 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> l < w
26 anlr 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> 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 = l |> a -> l < w -> pl
35 25, 34 mpd 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> 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 = l |> a -> pl -> ps
39 35, 38 mpd 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> ps
40 22, 39 mpbird 
G /\ A. z (z < w -> [z / x] px) /\ w = l |> a -> [w / x] px
41 40 exp 
G /\ A. z (z < w -> [z / x] px) -> w = l |> a -> [w / x] px
42 41 anwl 
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> w = l |> a -> [w / x] px
43 42 eexd 
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. a w = l |> a -> [w / x] px
44 43 eexd 
G /\ A. z (z < w -> [z / x] px) /\ ~w = 0 -> E. l E. a w = l |> a -> [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)