Theorem snocinj ≪ | index | src | ≫ 

theorem snocinj (a b l1 l2: nat): $ l1 |> a = l2 |> b <-> l1 = l2 /\ a = b $;
StepHypRefExpression
1 bitr3 
(rev (a : rev l1) = rev (b : rev l2) <-> l1 |> a = l2 |> b) ->
  (rev (a : rev l1) = rev (b : rev l2) <-> l1 = l2 /\ a = b) ->
  (l1 |> a = l2 |> b <-> l1 = l2 /\ a = b)
2 eqeq 
rev (a : rev l1) = l1 |> a -> rev (b : rev l2) = l2 |> b -> (rev (a : rev l1) = rev (b : rev l2) <-> l1 |> a = l2 |> b)
3 eqtr 
rev (a : rev l1) = rev (rev l1) |> a -> rev (rev l1) |> a = l1 |> a -> rev (a : rev l1) = l1 |> a
4 revS 
rev (a : rev l1) = rev (rev l1) |> a
5 3, 4 ax_mp 
rev (rev l1) |> a = l1 |> a -> rev (a : rev l1) = l1 |> a
6 snoceq1 
rev (rev l1) = l1 -> rev (rev l1) |> a = l1 |> a
7 revrev 
rev (rev l1) = l1
8 6, 7 ax_mp 
rev (rev l1) |> a = l1 |> a
9 5, 8 ax_mp 
rev (a : rev l1) = l1 |> a
10 2, 9 ax_mp 
rev (b : rev l2) = l2 |> b -> (rev (a : rev l1) = rev (b : rev l2) <-> l1 |> a = l2 |> b)
11 eqtr 
rev (b : rev l2) = rev (rev l2) |> b -> rev (rev l2) |> b = l2 |> b -> rev (b : rev l2) = l2 |> b
12 revS 
rev (b : rev l2) = rev (rev l2) |> b
13 11, 12 ax_mp 
rev (rev l2) |> b = l2 |> b -> rev (b : rev l2) = l2 |> b
14 snoceq1 
rev (rev l2) = l2 -> rev (rev l2) |> b = l2 |> b
15 revrev 
rev (rev l2) = l2
16 14, 15 ax_mp 
rev (rev l2) |> b = l2 |> b
17 13, 16 ax_mp 
rev (b : rev l2) = l2 |> b
18 10, 17 ax_mp 
rev (a : rev l1) = rev (b : rev l2) <-> l1 |> a = l2 |> b
19 1, 18 ax_mp 
(rev (a : rev l1) = rev (b : rev l2) <-> l1 = l2 /\ a = b) -> (l1 |> a = l2 |> b <-> l1 = l2 /\ a = b)
20 bitr 
(rev (a : rev l1) = rev (b : rev l2) <-> a : rev l1 = b : rev l2) ->
  (a : rev l1 = b : rev l2 <-> l1 = l2 /\ a = b) ->
  (rev (a : rev l1) = rev (b : rev l2) <-> l1 = l2 /\ a = b)
21 revinj 
rev (a : rev l1) = rev (b : rev l2) <-> a : rev l1 = b : rev l2
22 20, 21 ax_mp 
(a : rev l1 = b : rev l2 <-> l1 = l2 /\ a = b) -> (rev (a : rev l1) = rev (b : rev l2) <-> l1 = l2 /\ a = b)
23 bitr 
(a : rev l1 = b : rev l2 <-> a = b /\ rev l1 = rev l2) -> (a = b /\ rev l1 = rev l2 <-> l1 = l2 /\ a = b) -> (a : rev l1 = b : rev l2 <-> l1 = l2 /\ a = b)
24 consinj 
a : rev l1 = b : rev l2 <-> a = b /\ rev l1 = rev l2
25 23, 24 ax_mp 
(a = b /\ rev l1 = rev l2 <-> l1 = l2 /\ a = b) -> (a : rev l1 = b : rev l2 <-> l1 = l2 /\ a = b)
26 bitr 
(a = b /\ rev l1 = rev l2 <-> rev l1 = rev l2 /\ a = b) -> (rev l1 = rev l2 /\ a = b <-> l1 = l2 /\ a = b) -> (a = b /\ rev l1 = rev l2 <-> l1 = l2 /\ a = b)
27 ancomb 
a = b /\ rev l1 = rev l2 <-> rev l1 = rev l2 /\ a = b
28 26, 27 ax_mp 
(rev l1 = rev l2 /\ a = b <-> l1 = l2 /\ a = b) -> (a = b /\ rev l1 = rev l2 <-> l1 = l2 /\ a = b)
29 revinj 
rev l1 = rev l2 <-> l1 = l2
30 29 aneq1i 
rev l1 = rev l2 /\ a = b <-> l1 = l2 /\ a = b
31 28, 30 ax_mp 
a = b /\ rev l1 = rev l2 <-> l1 = l2 /\ a = b
32 25, 31 ax_mp 
a : rev l1 = b : rev l2 <-> l1 = l2 /\ a = b
33 22, 32 ax_mp 
rev (a : rev l1) = rev (b : rev l2) <-> l1 = l2 /\ a = b
34 19, 33 ax_mp 
l1 |> a = l2 |> b <-> l1 = l2 /\ a = b

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)