Theorem maplen ≪ | index | src | ≫ 

theorem maplen (F: set) (l: nat): $ len (map F l) = len l $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 mapeq2d 
_1 = l -> map F _1 = map F l
3 2 leneqd 
_1 = l -> len (map F _1) = len (map F l)
4 1 leneqd 
_1 = l -> len _1 = len l
5 3, 4 eqeqd 
_1 = l -> (len (map F _1) = len _1 <-> len (map F l) = len l)
6 id 
_1 = 0 -> _1 = 0
7 6 mapeq2d 
_1 = 0 -> map F _1 = map F 0
8 7 leneqd 
_1 = 0 -> len (map F _1) = len (map F 0)
9 6 leneqd 
_1 = 0 -> len _1 = len 0
10 8, 9 eqeqd 
_1 = 0 -> (len (map F _1) = len _1 <-> len (map F 0) = len 0)
11 id 
_1 = a2 -> _1 = a2
12 11 mapeq2d 
_1 = a2 -> map F _1 = map F a2
13 12 leneqd 
_1 = a2 -> len (map F _1) = len (map F a2)
14 11 leneqd 
_1 = a2 -> len _1 = len a2
15 13, 14 eqeqd 
_1 = a2 -> (len (map F _1) = len _1 <-> len (map F a2) = len a2)
16 id 
_1 = a1 : a2 -> _1 = a1 : a2
17 16 mapeq2d 
_1 = a1 : a2 -> map F _1 = map F (a1 : a2)
18 17 leneqd 
_1 = a1 : a2 -> len (map F _1) = len (map F (a1 : a2))
19 16 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
20 18, 19 eqeqd 
_1 = a1 : a2 -> (len (map F _1) = len _1 <-> len (map F (a1 : a2)) = len (a1 : a2))
21 leneq 
map F 0 = 0 -> len (map F 0) = len 0
22 map0 
map F 0 = 0
23 21, 22 ax_mp 
len (map F 0) = len 0
24 eqtr 
len (map F (a1 : a2)) = len (F @ a1 : map F a2) -> len (F @ a1 : map F a2) = suc (len (map F a2)) -> len (map F (a1 : a2)) = suc (len (map F a2))
25 leneq 
map F (a1 : a2) = F @ a1 : map F a2 -> len (map F (a1 : a2)) = len (F @ a1 : map F a2)
26 mapS 
map F (a1 : a2) = F @ a1 : map F a2
27 25, 26 ax_mp 
len (map F (a1 : a2)) = len (F @ a1 : map F a2)
28 24, 27 ax_mp 
len (F @ a1 : map F a2) = suc (len (map F a2)) -> len (map F (a1 : a2)) = suc (len (map F a2))
29 lenS 
len (F @ a1 : map F a2) = suc (len (map F a2))
30 28, 29 ax_mp 
len (map F (a1 : a2)) = suc (len (map F a2))
31 lenS 
len (a1 : a2) = suc (len a2)
32 suceq 
len (map F a2) = len a2 -> suc (len (map F a2)) = suc (len a2)
33 30, 31, 32 eqtr4g 
len (map F a2) = len a2 -> len (map F (a1 : a2)) = len (a1 : a2)
34 5, 10, 15, 20, 23, 33 listind 
len (map F l) = len l

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)