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 eqidd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> l1 = l1
12 10, 11 ntheqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> nth _1 l1 = nth n l1
13 id 
_2 = a -> _2 = a
14 13 anwr 
G /\ _1 = n /\ _2 = a -> _2 = a
15 14 anwl 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _2 = a
16 15 suceqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> suc _2 = suc a
17 12, 16 eqeqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l1 = suc _2 <-> nth n l1 = suc a)
18 eqidd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> l2 = l2
19 10, 18 ntheqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> nth _1 l2 = nth n l2
20 id 
_3 = b -> _3 = b
21 20 anwr 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _3 = b
22 21 suceqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> suc _3 = suc b
23 19, 22 eqeqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (nth _1 l2 = suc _3 <-> nth n l2 = suc b)
24 15, 21 preqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> _2, _3 = a, b
25 eqsidd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> R == R
26 24, 25 eleqd 
G /\ _1 = n /\ _2 = a /\ _3 = b -> (_2, _3 e. R <-> a, b e. R)
27 23, 26 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)
28 17, 27 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)
29 28 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
30 29 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
31 30 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
32 31 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
33 6, 32 mpd 
G -> nth n l1 = suc a -> nth n l2 = suc b -> a, b e. R
34 2, 33 mpd 
G -> nth n l2 = suc b -> a, b e. R
35 1, 34 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)