Theorem mapeqg ≪ | index | src | ≫ 

theorem mapeqg (F G: set) (l: nat) {x: nat}:
  $ all {x | F @ x = G @ x} l -> map F l = map G l $;
StepHypRefExpression
1 alleq2 
a1 = l -> (all {x | F @ x = G @ x} a1 <-> all {x | F @ x = G @ x} l)
2 mapeq2 
a1 = l -> map F a1 = map F l
3 mapeq2 
a1 = l -> map G a1 = map G l
4 2, 3 eqeqd 
a1 = l -> (map F a1 = map G a1 <-> map F l = map G l)
5 1, 4 imeqd 
a1 = l -> (all {x | F @ x = G @ x} a1 -> map F a1 = map G a1 <-> all {x | F @ x = G @ x} l -> map F l = map G l)
6 alleq2 
a1 = 0 -> (all {x | F @ x = G @ x} a1 <-> all {x | F @ x = G @ x} 0)
7 mapeq2 
a1 = 0 -> map F a1 = map F 0
8 mapeq2 
a1 = 0 -> map G a1 = map G 0
9 7, 8 eqeqd 
a1 = 0 -> (map F a1 = map G a1 <-> map F 0 = map G 0)
10 6, 9 imeqd 
a1 = 0 -> (all {x | F @ x = G @ x} a1 -> map F a1 = map G a1 <-> all {x | F @ x = G @ x} 0 -> map F 0 = map G 0)
11 alleq2 
a1 = a3 -> (all {x | F @ x = G @ x} a1 <-> all {x | F @ x = G @ x} a3)
12 mapeq2 
a1 = a3 -> map F a1 = map F a3
13 mapeq2 
a1 = a3 -> map G a1 = map G a3
14 12, 13 eqeqd 
a1 = a3 -> (map F a1 = map G a1 <-> map F a3 = map G a3)
15 11, 14 imeqd 
a1 = a3 -> (all {x | F @ x = G @ x} a1 -> map F a1 = map G a1 <-> all {x | F @ x = G @ x} a3 -> map F a3 = map G a3)
16 alleq2 
a1 = a2 : a3 -> (all {x | F @ x = G @ x} a1 <-> all {x | F @ x = G @ x} (a2 : a3))
17 mapeq2 
a1 = a2 : a3 -> map F a1 = map F (a2 : a3)
18 mapeq2 
a1 = a2 : a3 -> map G a1 = map G (a2 : a3)
19 17, 18 eqeqd 
a1 = a2 : a3 -> (map F a1 = map G a1 <-> map F (a2 : a3) = map G (a2 : a3))
20 16, 19 imeqd 
a1 = a2 : a3 -> (all {x | F @ x = G @ x} a1 -> map F a1 = map G a1 <-> all {x | F @ x = G @ x} (a2 : a3) -> map F (a2 : a3) = map G (a2 : a3))
21 eqtr4 
map F 0 = 0 -> map G 0 = 0 -> map F 0 = map G 0
22 map0 
map F 0 = 0
23 21, 22 ax_mp 
map G 0 = 0 -> map F 0 = map G 0
24 map0 
map G 0 = 0
25 23, 24 ax_mp 
map F 0 = map G 0
26 25 a1i 
all {x | F @ x = G @ x} 0 -> map F 0 = map G 0
27 allS 
all {x | F @ x = G @ x} (a2 : a3) <-> a2 e. {x | F @ x = G @ x} /\ all {x | F @ x = G @ x} a3
28 anr 
a2 e. {x | F @ x = G @ x} /\ all {x | F @ x = G @ x} a3 -> all {x | F @ x = G @ x} a3
29 27, 28 sylbi 
all {x | F @ x = G @ x} (a2 : a3) -> all {x | F @ x = G @ x} a3
30 29 imim1i 
(all {x | F @ x = G @ x} a3 -> map F a3 = map G a3) -> all {x | F @ x = G @ x} (a2 : a3) -> map F a3 = map G a3
31 anl 
a2 e. {x | F @ x = G @ x} /\ all {x | F @ x = G @ x} a3 -> a2 e. {x | F @ x = G @ x}
32 27, 31 sylbi 
all {x | F @ x = G @ x} (a2 : a3) -> a2 e. {x | F @ x = G @ x}
33 mapS 
map F (a2 : a3) = F @ a2 : map F a3
34 mapS 
map G (a2 : a3) = G @ a2 : map G a3
35 appeq2 
x = a2 -> F @ x = F @ a2
36 appeq2 
x = a2 -> G @ x = G @ a2
37 35, 36 eqeqd 
x = a2 -> (F @ x = G @ x <-> F @ a2 = G @ a2)
38 37 elabe 
a2 e. {x | F @ x = G @ x} <-> F @ a2 = G @ a2
39 anl 
a2 e. {x | F @ x = G @ x} /\ map F a3 = map G a3 -> a2 e. {x | F @ x = G @ x}
40 38, 39 sylib 
a2 e. {x | F @ x = G @ x} /\ map F a3 = map G a3 -> F @ a2 = G @ a2
41 anr 
a2 e. {x | F @ x = G @ x} /\ map F a3 = map G a3 -> map F a3 = map G a3
42 40, 41 conseqd 
a2 e. {x | F @ x = G @ x} /\ map F a3 = map G a3 -> F @ a2 : map F a3 = G @ a2 : map G a3
43 33, 34, 42 eqtr4g 
a2 e. {x | F @ x = G @ x} /\ map F a3 = map G a3 -> map F (a2 : a3) = map G (a2 : a3)
44 43 exp 
a2 e. {x | F @ x = G @ x} -> map F a3 = map G a3 -> map F (a2 : a3) = map G (a2 : a3)
45 32, 44 rsyl 
all {x | F @ x = G @ x} (a2 : a3) -> map F a3 = map G a3 -> map F (a2 : a3) = map G (a2 : a3)
46 45 a2i 
(all {x | F @ x = G @ x} (a2 : a3) -> map F a3 = map G a3) -> all {x | F @ x = G @ x} (a2 : a3) -> map F (a2 : a3) = map G (a2 : a3)
47 30, 46 rsyl 
(all {x | F @ x = G @ x} a3 -> map F a3 = map G a3) -> all {x | F @ x = G @ x} (a2 : a3) -> map F (a2 : a3) = map G (a2 : a3)
48 5, 10, 15, 20, 26, 47 listind 
all {x | F @ x = G @ x} l -> map F l = map G 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)