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 eqidd 
_1 = l -> a3 = a3
8 id 
_1 = l -> _1 = l
9 7, 8 ntheqd 
_1 = l -> nth a3 _1 = nth a3 l
10 eqidd 
_1 = l -> suc a = suc a
11 9, 10 eqeqd 
_1 = l -> (nth a3 _1 = suc a <-> nth a3 l = suc a)
12 eqsidd 
_1 = l -> F == F
13 12, 8 mapeqd 
_1 = l -> map F _1 = map F l
14 7, 13 ntheqd 
_1 = l -> nth a3 (map F _1) = nth a3 (map F l)
15 eqidd 
_1 = l -> suc (F @ a) = suc (F @ a)
16 14, 15 eqeqd 
_1 = l -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F l) = suc (F @ a))
17 11, 16 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))
18 17 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)))
19 eqidd 
_1 = 0 -> a3 = a3
20 id 
_1 = 0 -> _1 = 0
21 19, 20 ntheqd 
_1 = 0 -> nth a3 _1 = nth a3 0
22 eqidd 
_1 = 0 -> suc a = suc a
23 21, 22 eqeqd 
_1 = 0 -> (nth a3 _1 = suc a <-> nth a3 0 = suc a)
24 eqsidd 
_1 = 0 -> F == F
25 24, 20 mapeqd 
_1 = 0 -> map F _1 = map F 0
26 19, 25 ntheqd 
_1 = 0 -> nth a3 (map F _1) = nth a3 (map F 0)
27 eqidd 
_1 = 0 -> suc (F @ a) = suc (F @ a)
28 26, 27 eqeqd 
_1 = 0 -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F 0) = suc (F @ a))
29 23, 28 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))
30 29 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)))
31 eqidd 
_1 = a2 -> a3 = a3
32 id 
_1 = a2 -> _1 = a2
33 31, 32 ntheqd 
_1 = a2 -> nth a3 _1 = nth a3 a2
34 eqidd 
_1 = a2 -> suc a = suc a
35 33, 34 eqeqd 
_1 = a2 -> (nth a3 _1 = suc a <-> nth a3 a2 = suc a)
36 eqsidd 
_1 = a2 -> F == F
37 36, 32 mapeqd 
_1 = a2 -> map F _1 = map F a2
38 31, 37 ntheqd 
_1 = a2 -> nth a3 (map F _1) = nth a3 (map F a2)
39 eqidd 
_1 = a2 -> suc (F @ a) = suc (F @ a)
40 38, 39 eqeqd 
_1 = a2 -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F a2) = suc (F @ a))
41 35, 40 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))
42 41 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)))
43 eqidd 
_1 = a1 : a2 -> a3 = a3
44 id 
_1 = a1 : a2 -> _1 = a1 : a2
45 43, 44 ntheqd 
_1 = a1 : a2 -> nth a3 _1 = nth a3 (a1 : a2)
46 eqidd 
_1 = a1 : a2 -> suc a = suc a
47 45, 46 eqeqd 
_1 = a1 : a2 -> (nth a3 _1 = suc a <-> nth a3 (a1 : a2) = suc a)
48 eqsidd 
_1 = a1 : a2 -> F == F
49 48, 44 mapeqd 
_1 = a1 : a2 -> map F _1 = map F (a1 : a2)
50 43, 49 ntheqd 
_1 = a1 : a2 -> nth a3 (map F _1) = nth a3 (map F (a1 : a2))
51 eqidd 
_1 = a1 : a2 -> suc (F @ a) = suc (F @ a)
52 50, 51 eqeqd 
_1 = a1 : a2 -> (nth a3 (map F _1) = suc (F @ a) <-> nth a3 (map F (a1 : a2)) = suc (F @ a))
53 47, 52 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))
54 53 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)))
55 absurd 
~nth a3 0 = suc a -> nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a)
56 sucne0 
nth a3 0 = suc a -> nth a3 0 != 0
57 56 conv ne 
nth a3 0 = suc a -> ~nth a3 0 = 0
58 nth0 
nth a3 0 = 0
59 57, 58 mt2 
~nth a3 0 = suc a
60 55, 59 ax_mp 
nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a)
61 60 ax_gen 
A. a3 (nth a3 0 = suc a -> nth a3 (map F 0) = suc (F @ a))
62 ntheq1 
a3 = a4 -> nth a3 a2 = nth a4 a2
63 62 eqeq1d 
a3 = a4 -> (nth a3 a2 = suc a <-> nth a4 a2 = suc a)
64 ntheq1 
a3 = a4 -> nth a3 (map F a2) = nth a4 (map F a2)
65 64 eqeq1d 
a3 = a4 -> (nth a3 (map F a2) = suc (F @ a) <-> nth a4 (map F a2) = suc (F @ a))
66 63, 65 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))
67 66 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))
68 nthZ 
nth 0 (F @ a1 : map F a2) = suc (F @ a1)
69 peano2 
suc a1 = suc a <-> a1 = a
70 appeq2 
a1 = a -> F @ a1 = F @ a
71 70 suceqd 
a1 = a -> suc (F @ a1) = suc (F @ a)
72 69, 71 sylbi 
suc a1 = suc a -> suc (F @ a1) = suc (F @ a)
73 68, 72 syl5eq 
suc a1 = suc a -> nth 0 (F @ a1 : map F a2) = suc (F @ a)
74 nthZ 
nth 0 (a1 : a2) = suc a1
75 ntheq1 
a3 = 0 -> nth a3 (a1 : a2) = nth 0 (a1 : a2)
76 74, 75 syl6eq 
a3 = 0 -> nth a3 (a1 : a2) = suc a1
77 76 eqeq1d 
a3 = 0 -> (nth a3 (a1 : a2) = suc a <-> suc a1 = suc a)
78 ntheq2 
map F (a1 : a2) = F @ a1 : map F a2 -> nth 0 (map F (a1 : a2)) = nth 0 (F @ a1 : map F a2)
79 mapS 
map F (a1 : a2) = F @ a1 : map F a2
80 78, 79 ax_mp 
nth 0 (map F (a1 : a2)) = nth 0 (F @ a1 : map F a2)
81 ntheq1 
a3 = 0 -> nth a3 (map F (a1 : a2)) = nth 0 (map F (a1 : a2))
82 80, 81 syl6eq 
a3 = 0 -> nth a3 (map F (a1 : a2)) = nth 0 (F @ a1 : map F a2)
83 82 eqeq1d 
a3 = 0 -> (nth a3 (map F (a1 : a2)) = suc (F @ a) <-> nth 0 (F @ a1 : map F a2) = suc (F @ a))
84 77, 83 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))
85 73, 84 mpbiri 
a3 = 0 -> nth a3 (a1 : a2) = suc a -> nth a3 (map F (a1 : a2)) = suc (F @ a)
86 85 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)
87 exsuc 
a3 != 0 <-> E. a4 a3 = suc a4
88 87 conv ne 
~a3 = 0 <-> E. a4 a3 = suc a4
89 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))
90 nthS 
nth (suc a4) (a1 : a2) = nth a4 a2
91 ntheq1 
a3 = suc a4 -> nth a3 (a1 : a2) = nth (suc a4) (a1 : a2)
92 90, 91 syl6eq 
a3 = suc a4 -> nth a3 (a1 : a2) = nth a4 a2
93 92 eqeq1d 
a3 = suc a4 -> (nth a3 (a1 : a2) = suc a <-> nth a4 a2 = suc a)
94 ntheq2 
map F (a1 : a2) = F @ a1 : map F a2 -> nth a3 (map F (a1 : a2)) = nth a3 (F @ a1 : map F a2)
95 94, 79 ax_mp 
nth a3 (map F (a1 : a2)) = nth a3 (F @ a1 : map F a2)
96 nthS 
nth (suc a4) (F @ a1 : map F a2) = nth a4 (map F a2)
97 ntheq1 
a3 = suc a4 -> nth a3 (F @ a1 : map F a2) = nth (suc a4) (F @ a1 : map F a2)
98 96, 97 syl6eq 
a3 = suc a4 -> nth a3 (F @ a1 : map F a2) = nth a4 (map F a2)
99 95, 98 syl5eq 
a3 = suc a4 -> nth a3 (map F (a1 : a2)) = nth a4 (map F a2)
100 99 eqeq1d 
a3 = suc a4 -> (nth a3 (map F (a1 : a2)) = suc (F @ a) <-> nth a4 (map F a2) = suc (F @ a))
101 93, 100 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))
102 101 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)
103 89, 102 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)
104 103 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)
105 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)
106 104, 105 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)
107 88, 106 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)
108 86, 107 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)
109 108 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))
110 67, 109 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))
111 18, 30, 42, 54, 61, 110 listind 
A. a3 (nth a3 l = suc a -> nth a3 (map F l) = suc (F @ a))
112 6, 111 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)