Theorem elall2 | index | src |

theorem elall2 (R: set) (l1 l2: nat) {n x y: nat}:
  $ l1, l2 e. all2 R <->
    len l1 = len l2 /\
      A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R) $;
StepHypRefExpression
1 id
_1 = l1 -> _1 = l1
2 1 anwl
_1 = l1 /\ _2 = l2 -> _1 = l1
3 2 leneqd
_1 = l1 /\ _2 = l2 -> len _1 = len l1
4 id
_2 = l2 -> _2 = l2
5 4 anwr
_1 = l1 /\ _2 = l2 -> _2 = l2
6 5 leneqd
_1 = l1 /\ _2 = l2 -> len _2 = len l2
7 3, 6 eqeqd
_1 = l1 /\ _2 = l2 -> (len _1 = len _2 <-> len l1 = len l2)
8 eqidd
_1 = l1 /\ _2 = l2 -> n = n
9 8, 2 ntheqd
_1 = l1 /\ _2 = l2 -> nth n _1 = nth n l1
10 eqidd
_1 = l1 /\ _2 = l2 -> suc x = suc x
11 9, 10 eqeqd
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x <-> nth n l1 = suc x)
12 8, 5 ntheqd
_1 = l1 /\ _2 = l2 -> nth n _2 = nth n l2
13 eqidd
_1 = l1 /\ _2 = l2 -> suc y = suc y
14 12, 13 eqeqd
_1 = l1 /\ _2 = l2 -> (nth n _2 = suc y <-> nth n l2 = suc y)
15 biidd
_1 = l1 /\ _2 = l2 -> (x, y e. R <-> x, y e. R)
16 14, 15 imeqd
_1 = l1 /\ _2 = l2 -> (nth n _2 = suc y -> x, y e. R <-> nth n l2 = suc y -> x, y e. R)
17 11, 16 imeqd
_1 = l1 /\ _2 = l2 -> (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R <-> nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)
18 17 aleqd
_1 = l1 /\ _2 = l2 -> (A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <-> A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R))
19 18 aleqd
_1 = l1 /\ _2 = l2 -> (A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <-> A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R))
20 19 aleqd
_1 = l1 /\ _2 = l2 ->
  (A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <-> A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R))
21 7, 20 aneqd
_1 = l1 /\ _2 = l2 ->
  (len _1 = len _2 /\ A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R) <->
    len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R))
22 21 elabed
_1 = l1 ->
  (l2 e. {_2 | len _1 = len _2 /\ A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R)} <->
    len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R))
23 22 elsabe
l1, l2 e. S\ _1, {_2 | len _1 = len _2 /\ A. n A. x A. y (nth n _1 = suc x -> nth n _2 = suc y -> x, y e. R)} <->
  len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)
24 23 conv all2
l1, l2 e. all2 R <-> len l1 = len l2 /\ A. n A. x A. y (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)

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)