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 allnth 
all A l2 <-> A. n A. a1 (nth n l2 = suc a1 -> a1 e. A)
2 elall22 
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 biidd 
x = a2 -> (a1 e. A <-> a1 e. A)
4 3 elsabe 
a2, a1 e. S\ x, A <-> a1 e. A
5 4 raleqi 
A. a1 (nth n l2 = suc a1 -> a2, a1 e. S\ x, A) <-> A. a1 (nth n l2 = suc a1 -> a1 e. A)
6 5 raleqi 
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 ralcomb 
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 eexb 
E. a2 nth n l1 = suc a2 -> a1 e. A <-> A. a2 (nth n l1 = suc a2 -> a1 e. A)
9 mpcom 
E. a2 nth n l1 = suc a2 -> (E. a2 nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
10 exsuc 
nth n l1 != 0 <-> E. a2 nth n l1 = suc a2
11 nthne0 
nth n l1 != 0 <-> n < len l1
12 anl 
len l1 = len l2 /\ nth n l2 = suc a1 -> len l1 = len l2
13 12 lteq2d 
len l1 = len l2 /\ nth n l2 = suc a1 -> (n < len l1 <-> n < len l2)
14 nthne0 
nth n l2 != 0 <-> n < len l2
15 sucne0 
nth n l2 = suc a1 -> nth n l2 != 0
16 14, 15 sylib 
nth n l2 = suc a1 -> n < len l2
17 16 anwr 
len l1 = len l2 /\ nth n l2 = suc a1 -> n < len l2
18 13, 17 mpbird 
len l1 = len l2 /\ nth n l2 = suc a1 -> n < len l1
19 11, 18 sylibr 
len l1 = len l2 /\ nth n l2 = suc a1 -> nth n l1 != 0
20 10, 19 sylib 
len l1 = len l2 /\ nth n l2 = suc a1 -> E. a2 nth n l1 = suc a2
21 9, 20 syl 
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 syl5bir 
len l1 = len l2 /\ nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
23 22 exp 
len l1 = len l2 -> nth n l2 = suc a1 -> A. a2 (nth n l1 = suc a2 -> a1 e. A) -> a1 e. A
24 23 a2d 
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 24 alimd 
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 syl5bi 
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 syl5bi 
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 27 alimd 
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 28 imp 
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 sylbi 
l1, l2 e. all2 (S\ x, A) -> A. n A. a1 (nth n l2 = suc a1 -> a1 e. A)
31 1, 30 sylibr 
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)