Theorem mapnth ≪ | index | src | ≫ 

theorem mapnth (F: set) (a l n: nat):
  $ nth n l = suc a -> nth n (map F l) = suc (F @ a) $;
StepHypRefExpression
1 ntheq1 
a3 = n -> nth a3 l = nth n l
2 1 eqeq1d 
a3 = n -> (nth a3 l = suc a <-> nth n l = suc a)
3 ntheq1 
a3 = n -> nth a3 (map F l) = nth n (map F l)
4 3 eqeq1d 
a3 = n -> (nth a3 (map F l) = suc (F @ a) <-> nth n (map F l) = suc (F @ a))
5 2, 4 imeqd 
a3 = n -> (nth a3 l = suc a -> nth a3 (map F l) = suc (F @ a) <-> nth n l = suc a -> nth n (map F l) = suc (F @ a))
6 5 eale 
A. a3 (nth a3 l = suc a -> nth a3 (map F l) = suc (F @ a)) -> nth n l = suc a -> nth n (map F l) = suc (F @ a)
7 id 
_1 = l -> _1 = l
8 7 ntheq2d 
_1 = l -> nth a3 _1 = nth a3 l
9 8 eqeq1d 
_1 = l -> (nth a3 _1 = suc a <-> nth a3 l = suc a)
10 7 mapeq2d 
_1 = l -> map F _1 = map F l
11 10 ntheq2d 
_1 = l -> nth a3 (map F _1) = nth a3 (map F l)
12 11 eqeq1d 
_1 = l -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F l) = suc (F @ a))
13 9, 12 imeqd 
_1 = l -> (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a) <-> nth a3 l = suc a -> nth a3 (map F l) = suc (F @ a))
14 13 aleqd 
_1 = l -> (A. a3 (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a)) <-> A. a3 (nth a3 l = suc a -> nth a3 (map F l) = suc (F @ a)))
15 id 
_1 = 0 -> _1 = 0
16 15 ntheq2d 
_1 = 0 -> nth a3 _1 = nth a3 0
17 16 eqeq1d 
_1 = 0 -> (nth a3 _1 = suc a <-> nth a3 0 = suc a)
18 15 mapeq2d 
_1 = 0 -> map F _1 = map F 0
19 18 ntheq2d 
_1 = 0 -> nth a3 (map F _1) = nth a3 (map F 0)
20 19 eqeq1d 
_1 = 0 -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F 0) = suc (F @ a))
21 17, 20 imeqd 
_1 = 0 -> (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a) <-> nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a))
22 21 aleqd 
_1 = 0 -> (A. a3 (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a)) <-> A. a3 (nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a)))
23 id 
_1 = a2 -> _1 = a2
24 23 ntheq2d 
_1 = a2 -> nth a3 _1 = nth a3 a2
25 24 eqeq1d 
_1 = a2 -> (nth a3 _1 = suc a <-> nth a3 a2 = suc a)
26 23 mapeq2d 
_1 = a2 -> map F _1 = map F a2
27 26 ntheq2d 
_1 = a2 -> nth a3 (map F _1) = nth a3 (map F a2)
28 27 eqeq1d 
_1 = a2 -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F a2) = suc (F @ a))
29 25, 28 imeqd 
_1 = a2 -> (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a) <-> nth a3 a2 = suc a -> nth a3 (map F a2) = suc (F @ a))
30 29 aleqd 
_1 = a2 -> (A. a3 (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a)) <-> A. a3 (nth a3 a2 = suc a -> nth a3 (map F a2) = suc (F @ a)))
31 id 
_1 = a1 : a2 -> _1 = a1 : a2
32 31 ntheq2d 
_1 = a1 : a2 -> nth a3 _1 = nth a3 (a1 : a2)
33 32 eqeq1d 
_1 = a1 : a2 -> (nth a3 _1 = suc a <-> nth a3 (a1 : a2) = suc a)
34 31 mapeq2d 
_1 = a1 : a2 -> map F _1 = map F (a1 : a2)
35 34 ntheq2d 
_1 = a1 : a2 -> nth a3 (map F _1) = nth a3 (map F (a1 : a2))
36 35 eqeq1d 
_1 = a1 : a2 -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F (a1 : a2)) = suc (F @ a))
37 33, 36 imeqd 
_1 = a1 : a2 -> (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a) <-> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a))
38 37 aleqd 
_1 = a1 : a2 -> (A. a3 (nth a3 _1 = suc a -> nth a3 (map F _1) = suc (F @ a)) <-> A. a3 (nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)))
39 absurd 
~nth a3 0 = suc a -> nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a)
40 sucne0 
nth a3 0 = suc a -> nth a3 0 != 0
41 40 conv ne 
nth a3 0 = suc a -> ~nth a3 0 = 0
42 nth0 
nth a3 0 = 0
43 41, 42 mt2 
~nth a3 0 = suc a
44 39, 43 ax_mp 
nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a)
45 44 ax_gen 
A. a3 (nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a))
46 ntheq1 
a3 = a4 -> nth a3 a2 = nth a4 a2
47 46 eqeq1d 
a3 = a4 -> (nth a3 a2 = suc a <-> nth a4 a2 = suc a)
48 ntheq1 
a3 = a4 -> nth a3 (map F a2) = nth a4 (map F a2)
49 48 eqeq1d 
a3 = a4 -> (nth a3 (map F a2) = suc (F @ a) <-> nth a4 (map F a2) = suc (F @ a))
50 47, 49 imeqd 
a3 = a4 -> (nth a3 a2 = suc a -> nth a3 (map F a2) = suc (F @ a) <-> nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a))
51 50 cbval 
A. a3 (nth a3 a2 = suc a -> nth a3 (map F a2) = suc (F @ a)) <-> A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a))
52 nthZ 
nth 0 (F @ a1 : map F a2) = suc (F @ a1)
53 peano2 
suc a1 = suc a <-> a1 = a
54 appeq2 
a1 = a -> F @ a1 = F @ a
55 54 suceqd 
a1 = a -> suc (F @ a1) = suc (F @ a)
56 53, 55 sylbi 
suc a1 = suc a -> suc (F @ a1) = suc (F @ a)
57 52, 56 syl5eq 
suc a1 = suc a -> nth 0 (F @ a1 : map F a2) = suc (F @ a)
58 nthZ 
nth 0 (a1 : a2) = suc a1
59 ntheq1 
a3 = 0 -> nth a3 (a1 : a2) = nth 0 (a1 : a2)
60 58, 59 syl6eq 
a3 = 0 -> nth a3 (a1 : a2) = suc a1
61 60 eqeq1d 
a3 = 0 -> (nth a3 (a1 : a2) = suc a <-> suc a1 = suc a)
62 ntheq2 
map F (a1 : a2) = F @ a1 : map F a2 -> nth 0 (map F (a1 : a2)) = nth 0 (F @ a1 : map F a2)
63 mapS 
map F (a1 : a2) = F @ a1 : map F a2
64 62, 63 ax_mp 
nth 0 (map F (a1 : a2)) = nth 0 (F @ a1 : map F a2)
65 ntheq1 
a3 = 0 -> nth a3 (map F (a1 : a2)) = nth 0 (map F (a1 : a2))
66 64, 65 syl6eq 
a3 = 0 -> nth a3 (map F (a1 : a2)) = nth 0 (F @ a1 : map F a2)
67 66 eqeq1d 
a3 = 0 -> (nth a3 (map F (a1 : a2)) = suc (F @ a) <-> nth 0 (F @ a1 : map F a2) = suc (F @ a))
68 61, 67 imeqd 
a3 = 0 -> (nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a) <-> suc a1 = suc a -> nth 0 (F @ a1 : map F a2) = suc (F @ a))
69 57, 68 mpbiri 
a3 = 0 -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
70 69 a1i 
A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) -> a3 = 0 -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
71 exsuc 
a3 != 0 <-> E. a4 a3 = suc a4
72 71 conv ne 
~a3 = 0 <-> E. a4 a3 = suc a4
73 ancom 
(nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) /\ a3 = suc a4 -> a3 = suc a4 /\ (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a))
74 nthS 
nth (suc a4) (a1 : a2) = nth a4 a2
75 ntheq1 
a3 = suc a4 -> nth a3 (a1 : a2) = nth (suc a4) (a1 : a2)
76 74, 75 syl6eq 
a3 = suc a4 -> nth a3 (a1 : a2) = nth a4 a2
77 76 eqeq1d 
a3 = suc a4 -> (nth a3 (a1 : a2) = suc a <-> nth a4 a2 = suc a)
78 ntheq2 
map F (a1 : a2) = F @ a1 : map F a2 -> nth a3 (map F (a1 : a2)) = nth a3 (F @ a1 : map F a2)
79 78, 63 ax_mp 
nth a3 (map F (a1 : a2)) = nth a3 (F @ a1 : map F a2)
80 nthS 
nth (suc a4) (F @ a1 : map F a2) = nth a4 (map F a2)
81 ntheq1 
a3 = suc a4 -> nth a3 (F @ a1 : map F a2) = nth (suc a4) (F @ a1 : map F a2)
82 80, 81 syl6eq 
a3 = suc a4 -> nth a3 (F @ a1 : map F a2) = nth a4 (map F a2)
83 79, 82 syl5eq 
a3 = suc a4 -> nth a3 (map F (a1 : a2)) = nth a4 (map F a2)
84 83 eqeq1d 
a3 = suc a4 -> (nth a3 (map F (a1 : a2)) = suc (F @ a) <-> nth a4 (map F a2) = suc (F @ a))
85 77, 84 imeqd 
a3 = suc a4 -> (nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a) <-> nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a))
86 85 bi2a 
a3 = suc a4 /\ (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
87 73, 86 rsyl 
(nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) /\ a3 = suc a4 -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
88 87 eex 
E. a4 ((nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) /\ a3 = suc a4) -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
89 alexan 
A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) ->
  E. a4 a3 = suc a4 ->
  E. a4 ((nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) /\ a3 = suc a4)
90 88, 89 syl6 
A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) -> E. a4 a3 = suc a4 -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
91 72, 90 syl5bi 
A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) -> ~a3 = 0 -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
92 70, 91 casesd 
A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
93 92 iald 
A. a4 (nth a4 a2 = suc a -> nth a4 (map F a2) = suc (F @ a)) -> A. a3 (nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a))
94 51, 93 sylbi 
A. a3 (nth a3 a2 = suc a -> nth a3 (map F a2) = suc (F @ a)) -> A. a3 (nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a))
95 14, 22, 30, 38, 45, 94 listind 
A. a3 (nth a3 l = suc a -> nth a3 (map F l) = suc (F @ a))
96 6, 95 ax_mp 
nth n l = suc a -> nth n (map F l) = suc (F @ a)

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)