Theorem mapnthb ≪ | index | src | ≫ 

theorem mapnthb (F: set) {a: nat} (b l n: nat):
  $ nth n (map F l) = suc b <-> E. a (nth n l = suc a /\ b = F @ a) $;
StepHypRefExpression
1 exsuc 
nth n l != 0 <-> E. a nth n l = suc a
2 nthne0 
nth n l != 0 <-> n < len l
3 lteq2 
len (map F l) = len l -> (n < len (map F l) <-> n < len l)
4 maplen 
len (map F l) = len l
5 3, 4 ax_mp 
n < len (map F l) <-> n < len l
6 nthne0 
nth n (map F l) != 0 <-> n < len (map F l)
7 sucne0 
nth n (map F l) = suc b -> nth n (map F l) != 0
8 6, 7 sylib 
nth n (map F l) = suc b -> n < len (map F l)
9 5, 8 sylib 
nth n (map F l) = suc b -> n < len l
10 2, 9 sylibr 
nth n (map F l) = suc b -> nth n l != 0
11 1, 10 sylib 
nth n (map F l) = suc b -> E. a nth n l = suc a
12 anr 
nth n (map F l) = suc b /\ nth n l = suc a -> nth n l = suc a
13 peano2 
suc b = suc (F @ a) <-> b = F @ a
14 anl 
nth n (map F l) = suc b /\ nth n l = suc a -> nth n (map F l) = suc b
15 mapnth 
nth n l = suc a -> nth n (map F l) = suc (F @ a)
16 15 anwr 
nth n (map F l) = suc b /\ nth n l = suc a -> nth n (map F l) = suc (F @ a)
17 14, 16 eqtr3d 
nth n (map F l) = suc b /\ nth n l = suc a -> suc b = suc (F @ a)
18 13, 17 sylib 
nth n (map F l) = suc b /\ nth n l = suc a -> b = F @ a
19 12, 18 iand 
nth n (map F l) = suc b /\ nth n l = suc a -> nth n l = suc a /\ b = F @ a
20 19 exp 
nth n (map F l) = suc b -> nth n l = suc a -> nth n l = suc a /\ b = F @ a
21 20 eximd 
nth n (map F l) = suc b -> E. a nth n l = suc a -> E. a (nth n l = suc a /\ b = F @ a)
22 11, 21 mpd 
nth n (map F l) = suc b -> E. a (nth n l = suc a /\ b = F @ a)
23 15 anwl 
nth n l = suc a /\ b = F @ a -> nth n (map F l) = suc (F @ a)
24 anr 
nth n l = suc a /\ b = F @ a -> b = F @ a
25 24 suceqd 
nth n l = suc a /\ b = F @ a -> suc b = suc (F @ a)
26 23, 25 eqtr4d 
nth n l = suc a /\ b = F @ a -> nth n (map F l) = suc b
27 26 eex 
E. a (nth n l = suc a /\ b = F @ a) -> nth n (map F l) = suc b
28 22, 27 ibii 
nth n (map F l) = suc b <-> E. a (nth n l = suc a /\ b = 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)