Theorem maplen ≪ | index | src | ≫ 

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