Theorem all2i ≪ | index | src | ≫ 

theorem all2i (G: wff) (R: set) (a b l1 l2 n: nat):
  $ G -> nth n l1 = suc a $ >
  $ G -> nth n l2 = suc b $ >
  $ G -> l1, l2 e. all2 R $ >
  $ G -> a, b e. R $;
StepHypRefExpression
1 hyp h2 
G -> nth n l2 = suc b
2 hyp h1 
G -> nth n l1 = suc a
3 elall2 
l1, l2 e. all2 R <-> len l1 = len l2 /\ A. _1 A. _2 A. _3 (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R)
4 hyp h 
G -> l1, l2 e. all2 R
5 3, 4 sylib 
G -> len l1 = len l2 /\ A. _1 A. _2 A. _3 (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R)
6 5 anrd 
G -> A. _1 A. _2 A. _3 (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R)
7 id 
_1 = n -> _1 = n
8 7 anwr 
G /\ _1 = n -> _1 = n
9 8 anwl 
G /\ _1 = n /\ _2 = a -> _1 = n
10 9 anwl 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _1 = n
11 10 ntheq1d 
G /\ _1 = n /\ _2 = a /\ _3 = b -> nth _1 l1 = nth n l1
12 id 
_2 = a -> _2 = a
13 12 anwr 
G /\ _1 = n /\ _2 = a -> _2 = a
14 13 anwl 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _2 = a
15 14 suceqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> suc _2 = suc a
16 11, 15 eqeqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l1 = suc _2 <-> nth n l1 = suc a)
17 10 ntheq1d 
G /\ _1 = n /\ _2 = a /\ _3 = b -> nth _1 l2 = nth n l2
18 id 
_3 = b -> _3 = b
19 18 anwr 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _3 = b
20 19 suceqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> suc _3 = suc b
21 17, 20 eqeqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l2 = suc _3 <-> nth n l2 = suc b)
22 14, 19 preqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _2, _3 = a, b
23 22 eleq1d 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (_2, _3 e. R <-> a, b e. R)
24 21, 23 imeqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l2 = suc _3 -> _2, _3 e. R <-> nth n l2 = suc b -> a, b e. R)
25 16, 24 imeqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R <-> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R)
26 25 bi1d 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R) -> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R
27 26 ealde 
G /\ _1 = n /\ _2 = a -> A. _3 (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R) -> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R
28 27 ealde 
G /\ _1 = n -> A. _2 A. _3 (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R) -> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R
29 28 ealde 
G -> A. _1 A. _2 A. _3 (nth _1 l1 = suc _2 -> nth _1 l2 = suc _3 -> _2, _3 e. R) -> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R
30 6, 29 mpd 
G -> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R
31 2, 30 mpd 
G -> nth n l2 = suc b -> a, b e. R
32 1, 31 mpd 
G -> a, b e. R

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)