Theorem all2rev1 ≪ | index | src | ≫ 

theorem all2rev1 (R: set) (l1 l2: nat):
  $ l1, l2 e. all2 R -> rev l1, rev l2 e. all2 R $;
StepHypRefExpression
1 elall2 
rev l1, rev l2 e. all2 R <-> len (rev l1) = len (rev l2) /\ A. a1 A. a2 A. a3 (nth a1 (rev l1) = suc a2 -> nth a1 (rev l2) = suc a3 -> a2, a3 e. R)
2 revlen 
len (rev l1) = len l1
3 revlen 
len (rev l2) = len l2
4 all2len 
l1, l2 e. all2 R -> len l1 = len l2
5 3, 4 syl6eqr 
l1, l2 e. all2 R -> len l1 = len (rev l2)
6 2, 5 syl5eq 
l1, l2 e. all2 R -> len (rev l1) = len (rev l2)
7 revnth 
a1 < len l1 -> nth a1 (rev l1) = nth (len l1 - suc a1) l1
8 lteq2 
len (rev l1) = len l1 -> (a1 < len (rev l1) <-> a1 < len l1)
9 8, 2 ax_mp 
a1 < len (rev l1) <-> a1 < len l1
10 anlr 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth a1 (rev l1) = suc a2
11 nthSlt 
nth a1 (rev l1) = suc a2 -> a1 < len (rev l1)
12 10, 11 rsyl 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> a1 < len (rev l1)
13 9, 12 sylib 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> a1 < len l1
14 7, 13 syl 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth a1 (rev l1) = nth (len l1 - suc a1) l1
15 14, 10 eqtr3d 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth (len l1 - suc a1) l1 = suc a2
16 4 anwll 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> len l1 = len l2
17 16 subeq1d 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> len l1 - suc a1 = len l2 - suc a1
18 17 ntheq1d 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth (len l1 - suc a1) l2 = nth (len l2 - suc a1) l2
19 revnth 
a1 < len l2 -> nth a1 (rev l2) = nth (len l2 - suc a1) l2
20 lteq2 
len (rev l2) = len l2 -> (a1 < len (rev l2) <-> a1 < len l2)
21 20, 3 ax_mp 
a1 < len (rev l2) <-> a1 < len l2
22 anr 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth a1 (rev l2) = suc a3
23 nthSlt 
nth a1 (rev l2) = suc a3 -> a1 < len (rev l2)
24 22, 23 rsyl 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> a1 < len (rev l2)
25 21, 24 sylib 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> a1 < len l2
26 19, 25 syl 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth a1 (rev l2) = nth (len l2 - suc a1) l2
27 26, 22 eqtr3d 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth (len l2 - suc a1) l2 = suc a3
28 18, 27 eqtrd 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> nth (len l1 - suc a1) l2 = suc a3
29 anll 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> l1, l2 e. all2 R
30 15, 28, 29 all2i 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 /\ nth a1 (rev l2) = suc a3 -> a2, a3 e. R
31 30 exp 
l1, l2 e. all2 R /\ nth a1 (rev l1) = suc a2 -> nth a1 (rev l2) = suc a3 -> a2, a3 e. R
32 31 ialda 
l1, l2 e. all2 R -> A. a3 (nth a1 (rev l1) = suc a2 -> nth a1 (rev l2) = suc a3 -> a2, a3 e. R)
33 32 iald 
l1, l2 e. all2 R -> A. a2 A. a3 (nth a1 (rev l1) = suc a2 -> nth a1 (rev l2) = suc a3 -> a2, a3 e. R)
34 33 iald 
l1, l2 e. all2 R -> A. a1 A. a2 A. a3 (nth a1 (rev l1) = suc a2 -> nth a1 (rev l2) = suc a3 -> a2, a3 e. R)
35 6, 34 iand 
l1, l2 e. all2 R -> len (rev l1) = len (rev l2) /\ A. a1 A. a2 A. a3 (nth a1 (rev l1) = suc a2 -> nth a1 (rev l2) = suc a3 -> a2, a3 e. R)
36 1, 35 sylibr 
l1, l2 e. all2 R -> rev l1, rev l2 e. all2 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)