Theorem all2all2 ≪ | index | src | ≫ 

theorem all2all2 (A: set) (l1 l2: nat) {x: nat}:
  $ l1, l2 e. all2 (S\ x, A) -> all A l2 $;
StepHypRefExpression
1
 
all A l2 <-> A. n A. a1 (nth n l2 = suc a1 -> a1 e. A)
2
 
l1, l2 e. all2 (S\ x, A) <-> len l1 = len l2 /\ A. n A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A))
3
 
x = a2 -> (a1 e. A <-> a1 e. A)
4
 
a2, a1 e. S\ x, A <-> a1 e. A
5
 
A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A) <-> A. a1 (nth n l2 = suc a1 -> a1 e. A)
6
 
A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A)) <-> A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a1 e. A))
7
 
A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a1 e. A)) <-> A. a1 (nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A))
8
 
E. a2 nth n l1 = suc a2 -> a1 e. A <-> A. a2 (nth n l1 = suc a2 -> a1 e. A)
9
 
E. a2 nth n l1 = suc a2 -> (E. a2 nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
10
 
nth n l1 != 0 <-> E. a2 nth n l1 = suc a2
11
 
nth n l1 != 0 <-> n < len l1
12
 
len l1 = len l2 /\ nth n l2 = suc a1 -> len l1 = len l2
13
 
len l1 = len l2 /\ nth n l2 = suc a1 -> (n < len l1 <-> n < len l2)
14
 
nth n l2 != 0 <-> n < len l2
15
 
nth n l2 = suc a1 -> nth n l2 != 0
16
 
nth n l2 = suc a1 -> n < len l2
17
 
len l1 = len l2 /\ nth n l2 = suc a1 -> n < len l2
18
 
len l1 = len l2 /\ nth n l2 = suc a1 -> n < len l1
19
 
len l1 = len l2 /\ nth n l2 = suc a1 -> nth n l1 != 0
20
 
len l1 = len l2 /\ nth n l2 = suc a1 -> E. a2 nth n l1 = suc a2
21
9, 20
 
len l1 = len l2 /\ nth n l2 = suc a1 -> (E. a2 nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
22
8, 21
 
len l1 = len l2 /\ nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
23
 
len l1 = len l2 -> nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
24
 
len l1 = len l2 -> (nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A)) -> nth n l2 = suc a1 -> a1 e. A
25
 
len l1 = len l2 -> A. a1 (nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A)) -> A. a1 (nth n l2 = suc a1 -> a1 e. A)
26
7, 25
 
len l1 = len l2 -> A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a1 e. A)) -> A. a1 (nth n l2 = suc a1 -> a1 e. A)
27
6, 26
 
len l1 = len l2 -> A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A)) -> A. a1 (nth n l2 = suc a1 -> a1 e. A)
28
 
len l1 = len l2 -> A. n A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A)) -> A. n A. a1 (nth n l2 = suc a1 -> a1 e. A)
29
 
len l1 = len l2 /\ A. n A. a2 (nth n l1 = suc a2 -> A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A)) -> A. n A. a1 (nth n l2 = suc a1 -> a1 e. A)
30
2, 29
 
l1, l2 e. all2 (S\ x, A) -> A. n A. a1 (nth n l2 = suc a1 -> a1 e. A)
31
1, 30
 
l1, l2 e. all2 (S\ x, A) -> all A l2

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)